proposition: Lemma remove_eq : forall a x l, In a (remove x l) <-> a <> x /\ In a l.
proof: Proof. intuition. subst. eapply notin_remove. apply H. eapply remove_In. apply H. apply In_remove; auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)