proposition: Lemma Vforall2_map_intro : forall n (v : vector A n), Vforall (fun x => S (f x) (g x)) v -> Vforall2 S (Vmap f v) (Vmap g v).
proof: Proof. induction v; simpl; intros. refl. rewrite Vforall2_cons_eq. intuition. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)