proposition: Lemma Vnth_map2 : forall n (vl : vector A n) (vr : vector B n) i (ip : i < n), Vnth (Vmap2 vl vr) ip = f (Vnth vl ip) (Vnth vr ip).
proof: Proof. induction n; intros. VOtac. lia. VSntac vl. VSntac vr. destruct i. refl. simpl. apply IHn. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)