proposition: Lemma notin_replace x y xs : E.eq y x \/ ~In x (replace x y xs).
proof: Proof. Proof with auto with ordered_type. eq_dec y x... unfold replace. case_eq (mem x xs); intro hx; set_iff. right. split_all... right. rewrite not_mem_iff. hyp. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)