proposition: Lemma aeq_le_aeq_ch : aeq << aeq_ch.
proof: Proof. intro u; revert u. ind_size1 u; intros u' uu'; inv_aeq uu'; subst; ens. refl. refl. trans (App u v). apply mon_app_l. class. firstorder auto with crelations. fo. apply mon_app_r. class. fo. firstorder auto with crelations. rename x0 into y. rename u0 into v. set (xs := union (add x (union (fv u) (bv u))) (add y (union (fv v) (bv v)))). gen (var_notin_ok xs). set (z := var_notin xs). unfold xs. set_iff. intro hz. trans (replace_all x z (Lam x u)). apply rt_step. apply m_step. apply aeq_ch_top_intro; simpl; set_iff; fo. trans (replace_all y z (Lam y v)). 2:{ sym. apply rt_step. apply m_step. apply aeq_ch_top_intro; simpl; set_iff; fo. } simpl. rewrite !replace_var_eq. apply mon_lam. class. refl. apply hu. rewrite size_replace_all. refl. rewrite !replace_all_aeq_rename, i0, rename2; firstorder auto with crelations. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)