proposition: Lemma Vforall_impl : forall A (P Q : A -> Prop) n (v : vector A n), Vforall P v -> (forall x, Vin x v -> P x -> Q x) -> Vforall Q v.
proof: Proof. intros. apply Vforall_intro. intros. apply H0. hyp. eapply Vforall_in with (n := n). apply H. apply H1. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)