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