proposition: Lemma left_typing Gamma E L: Gamma ⊢₊₊ E : L -> Gamma ⊢₊ left_side E : L.
proof: Proof. induction 1; cbn; eauto. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)