proposition: Lemma Vforall2_cast n (u : vector A n) (v : vector B n) n' (h h' : n=n') : Vforall2 (Vcast u h) (Vcast v h') <-> Vforall2 u v.
proof: Proof. subst n'. rewrite !Vcast_refl. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)