proposition: Lemma replace2 x y z xs : x = y \/ ~In y xs -> replace y z (replace x y xs) [=] replace x z xs.
proof: Proof. intros [h|h]. subst. rewrite replace_idem. refl. unfold replace at -1. case_eq (mem x xs); intro hx. unfold replace. rewrite add_b, eqb_refl; simpl. rewrite remove_add_eq. eq_dec x y. apply add_m. refl. rewrite <- e, remove_idem. refl. rewrite remove_com, remove_equal with (x:=y). refl. hyp. unfold replace. rewrite not_mem_iff in h. rewrite h. refl. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)