proposition: Lemma replace_idem x xs : replace x x xs [=] xs.
proof: Proof. unfold replace. case_eq (mem x xs); intro hx. 2: refl. rewrite <- mem_iff in hx. intro a. set_iff. split_all. rewrite <- H. hyp. eq_dec x a; auto. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)