proposition: Lemma Vforall2_sub : forall n (v1 : vector A n) (v2 : vector B n) p q (h : p+q<=n), Vforall2 v1 v2 -> Vforall2 (Vsub v1 h) (Vsub v2 h).
proof: Proof. intros n v1 v2 p q h e. apply Vforall2_intro_nth; intros i hi. rewrite !Vnth_sub. apply Vforall2_elim_nth. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)