proposition: Lemma linearize_terms_ordertyping n Gamma (S: list (exp X)) L A: ord' L < n -> ord A <= n -> Gamma ⊢₊(n) S : L -> Gamma ⊢(n) linearize_terms S : (Arr (rev L) A) → A.
proof: Proof. intros H; econstructor; eapply AppR_ordertyping with (L := L). eapply orderlisttyping_preservation_under_renaming; eauto. intros x ?; cbn; eauto. econstructor; trivial; simplify; cbn; intuition. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)