proposition: Lemma Vforall_lforall : forall (A : Type) n (v : vector A n) (p : A -> Prop), Vforall p v -> lforall p (list_of_vec v).
proof: Proof. intros. gen H. induction v. trivial. intros lforall. red in lforall. destruct lforall as [pa vforall]. red. simpl. split. trivial. unfold lforall in IHv. apply IHv; trivial. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)