proposition: Lemma Vforall2_cons_eq : forall u v n (us : vector A n) (vs : vector B n), Vforall2 (Vcons u us) (Vcons v vs) <-> R u v /\ Vforall2 us vs.
proof: Proof. fo. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)