proposition: Lemma typing_combine Gamma E L: Gamma ⊢₊ left_side E : L -> Gamma ⊢₊ right_side E : L -> Gamma ⊢₊₊ 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 Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)