proposition: Lemma incl_cons_l : forall (a : A) l m, a :: l [= m -> In a m /\ l [= m.
proof: Proof. intros a l m. unfold incl. simpl. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)