proposition: Lemma lforall_intro : forall l, (forall x, In x l -> P x) -> lforall l.
proof: Proof. induction l; simpl; intros. exact I. split. apply H. auto. apply IHl. intros. apply H. auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)