proposition: Lemma Vforall2_tail : forall n (v1 : vector A (S n)) (v2 : vector B (S n)), Vforall2 v1 v2 -> Vforall2 (Vtail v1) (Vtail v2).
proof: Proof. intros. revert H. VSntac v1. VSntac v2. unfold Vforall2. simpl. tauto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)