proposition: Lemma incl_cons_l_in : forall (x : A) l m, x :: l [= m -> In x m.
proof: Proof. unfold incl. simpl. intros. apply H. left. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)