proposition: Lemma Vforall2_intro_nth : forall n (v1 : vector A n) (v2 : vector B n), (forall i (ip : i < n), R (Vnth v1 ip) (Vnth v2 ip)) -> Vforall2 v1 v2.
proof: Proof. unfold Vforall2. induction v1; intros. VOtac. simpl. auto. revert H. VSntac v2. intro. split. apply (H0 0 (Nat.lt_0_succ _)). apply IHv1. intros. assert (S i< S n). lia. ded (H0 _ H1). simpl in H2. assert (ip = NatCompat.lt_S_n H1). apply lt_unique. rewrite H3. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)