proposition: Lemma In_removes : forall x l m, In x (removes l m) <-> In x m /\ ~In x l.
proof: Proof. induction m; simpl; intros. tauto. case (In_dec a l); intro. rewrite IHm. fo. subst. contr. simpl. rewrite IHm. fo. subst. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)