proposition: Lemma strict_subset_rem a P : mem a P -> rem a P [<] P.
proof: Proof. intro aP. split. apply subset_rem. intro h. apply h in aP. revert aP. apply notin_rem. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)