proposition: Lemma add_rem (eq_dec : eq_dec_type) a P : mem a P -> add a (rem a P) [=] P.
proof: Proof. intros aP x. split. fo. subst. hyp. stac. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)