proposition: Lemma Vforall_incl : forall n1 (v1 : vector A n1) n2 (v2 : vector A n2), (forall x, Vin x v1 -> Vin x v2) -> Vforall v2 -> Vforall v1.
proof: Proof. intros. apply Vforall_intro. intros. apply Vforall_in with (v := v2). hyp. apply H. hyp. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)