proposition: Lemma aeq_kr_le_aeq : aeq_kr << aeq.
proof: Proof. intro u; revert u; induction 1. refl. refl. rewrite IHaeq_kr1, IHaeq_kr2. refl. pose (xs' := union xs (union (bv u) (union (bv u') (union (fv u) (fv u'))))). gen (var_notin_ok xs'). set (y := var_notin xs'). unfold xs'. set_iff. intro hy. rewrite aeq_alpha with (y:=y), aeq_alpha with (x:=x') (y:=y). 2: fo. 2: fo. apply Lam_aeq. refl. rewrite !rename1_no_alpha. fo. right. right. fo. right. right. fo. Qed.
imports: CoLoR(LogicUtil LAlpha RelUtil BoolUtil) Coq(Morphisms)