proposition: Lemma ordertyping_combine Gamma n E L: Gamma ⊢₊(n) left_side E : L -> Gamma ⊢₊(n) right_side E : L -> Gamma ⊢₊₊(n) E : L.
proof: Proof. intros H1 H2; induction E in L, H1, H2 |-*; inv H1; inv H2; trivial. destruct a; eauto. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)