proposition: Lemma replace_all_aeq_rename x y : forall u, ~In y (fv u) -> ~In y (bv u) -> replace_all x y u ~~ rename x y u.
proof: Proof. induction u; simpl; set_iff; intros h1 h2. rewrite rename_var. unfold Def.replace_var. eq_dec x0 x; refl. refl. rewrite rename_app, IHu1, IHu2; firstorder auto with crelations. rewrite IHu; [idtac|fo|fo]. unfold Def.replace_var. eq_dec x0 x. subst x0. rewrite rename_notin_fv with (u:=Lam x u). 2: simpl; set_iff; fo. sym. apply aeq_alpha. fo. rewrite rename_lam. eq_dec y x0. firstorder auto with exfalso. bool. eq_dec x0 x. fo. refl. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)