proposition: Lemma Vforall2_elim_nth : forall n (v1 : vector A n) (v2 : vector B n) i (ip : i < n), Vforall2 v1 v2 -> R (Vnth v1 ip) (Vnth v2 ip).
proof: Proof. induction v1; intros. absurd (i<0); lia. revert H. VSntac v2. unfold Vforall2. destruct i; simpl. tauto. intuition. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)