proposition: Lemma rem_add a P : ~mem a P -> rem a (add a P) [=] P.
proof: Proof. intros naP x. fo. intro; subst; contr. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)