proposition: Lemma Vforall2_cons_elim : forall n (u : vector A n) (v : vector B n) x y, Vforall2 (Vcons x u) (Vcons y v) -> Vforall2 u v.
proof: Proof. fo. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)