proposition: Lemma replace_all2 x y : forall u, ~In y (fv u) -> ~In y (bv u) -> replace_all y x (replace_all x y u) = u.
proof: Proof. induction u; simpl; set_iff; intros h1 h2. rewrite replace_var2. refl. fo. refl. f_equal; fo. f_equal. rewrite replace_var2. refl. fo. fo. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)