proposition: Lemma not_incl : forall l m, ~ l [= m <-> exists x:A, In x l /\ ~In x m.
proof: Proof. induction l; simpl; intros. intuition. absurd (nil[=m). hyp. apply incl_nil. do 2 destruct H. contr. split; intro. 2:{ do 3 destruct H. subst. intro. apply H0. apply H. left. refl. intro. absurd (In x m). hyp. apply H1. right. hyp. } case (In_dec eqA_dec a m); intro. assert (~l[=m). intro. apply H. unfold incl. intro b. simpl. intuition. rewrite IHl in H0. do 2 destruct H0. exists x. tauto. exists a. tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)