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