proposition: Lemma unify_typing E L sigma: E ↦ sigma -> all_terms (@lambda_free X) E -> Gamma ⊢₊₊(1) E : L -> Gamma ⊩(1) sigma : Gamma.
proof: Proof. Proof using HO. induction 1 in L |-*. - intros; now eapply var_typing. - intros LF T. eapply decomp'_typing in T as T'; eauto. eauto; destruct T' as [L' T']; inv T'; inv H7. specialize (IHunify L0); mp IHunify; [| mp IHunify]. + eapply decomp'_lambda_free in H; eauto. simplify in H; cbn in H. intuition idtac. eapply lambda_free_subst_eqs; eauto. intros y; unfold update; destruct eq_dec; subst; intros; eauto. + eapply eqs_ordertyping_preservation_subst; eauto. eapply update_typing; eauto; eapply var_typing; eauto. + eapply update_typing; [eauto| | eauto]. eapply ordertyping_weak_preservation_under_substitution; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)