proposition: Lemma lforall_eq : forall l, lforall l <-> (forall x, In x l -> P x).
proof: Proof. induction l; simpl; intuition. subst. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)