{P : Sort u} →
  {α : Type} →
    {decls : Array (Std.Sat.AIG.Decl α)} →
      {decl : Std.Sat.AIG.Decl α} →
        {t : Std.Sat.AIG.CacheHit decls decl} →
          {α' : Type} →
            {decls' : Array (Std.Sat.AIG.Decl α')} →
              {decl' : Std.Sat.AIG.Decl α'} →
                {t' : Std.Sat.AIG.CacheHit decls' decl'} →
                  α = α' → decls ≍ decls' → decl ≍ decl' → t ≍ t' → Std.Sat.AIG.CacheHit.noConfusionType P t t'