proposition: Lemma incl_remove : forall (x : A) l m, ~In x l -> l [= m -> l [= remove x m.
proof: Proof. induction l; simpl; intros. apply incl_nil. assert (~a=x /\ ~In x l). tauto. unfold incl. intros. simpl in H2. destruct H2. subst a0. apply In_remove. auto. unfold incl in H0. apply H0. simpl. auto. apply IHl. auto. apply incl_cons_l_incl with (x := a). exact H0. exact H2. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)