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