proposition: Lemma replace_var2 x y z : x = z \/ y <> z -> replace_var y x (replace_var x y z) = z.
proof: Proof. intro h. unfold Def.replace_var. eq_dec z x. subst. eq_dec y y. refl. cong. eq_dec z y. subst. fo. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)