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