proposition: Lemma aeq_le_aeq_kr : aeq << aeq_kr.
proof: Proof. intro u; revert u. ind_size1 u; intros t' tt'; inv_aeq tt'; subst. refl. refl. apply aeq_kr_app; firstorder auto with crelations. clear tt'. pose (xs := union (bv u) (bv u0)). apply aeq_kr_lam with (xs := xs); ens. intro y. unfold xs. set_iff. intro hy. apply hu. rewrite size_rename1. refl. rewrite <- !rename1_no_alpha, i0, rename2. refl. hyp. right. right. fo. right. right. fo. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)