proposition: Lemma aeq_equiv_mon : aeq == clos_equiv (clos_mon aeq_top).
proof: Proof. split; intros u v uv; revert u v uv. induction 1. refl. sym. hyp. trans v; hyp. clear uv. revert u u' IHuv. induction 1. apply e_step. apply m_app_l. hyp. refl. trans (App y v); hyp. sym. hyp. clear uv. revert v v' IHuv. induction 1. apply e_step. apply m_app_r. hyp. refl. trans (App u y); hyp. sym. hyp. clear uv. revert u u' IHuv. induction 1. apply e_step. apply m_lam. hyp. refl. trans (Lam x y); hyp. sym. hyp. apply e_step. apply m_step. apply aeq_top_intro. hyp. induction 1. revert x y H. induction 1. inversion H. apply aeq_alpha. hyp. apply aeq_app_l. hyp. apply aeq_app_r. hyp. apply aeq_lam. hyp. apply aeq_refl. apply aeq_trans with y; hyp. apply aeq_sym. hyp. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)