proposition: Lemma aeq_ch_le_aeq : aeq_ch << aeq.
proof: Proof. apply rtc_min. constructor; class. apply clos_mon_min. class. intros u v uv; inversion uv; clear uv; subst. rewrite replace_all_aeq_rename; [idtac|fo|fo]. rewrite rename_notin_fv; firstorder auto with crelations. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)