proposition: Lemma rem_add_neq a b P : a <> b -> rem a (add b P) [=] add b (rem a P).
proof: Proof. intro nab. split. fo. fo. subst. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)