proposition: Lemma remove_add_if x y xs : remove y (add x xs) [=] if eqb y x then remove y xs else add x (remove y xs).
proof: Proof. eq_dec y x. rewrite e at 1. rewrite remove_add_eq, e. refl. intro; set_iff; intuition. apply n. rewrite H, H0. refl. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)