proposition: Lemma linearize_terms_typing Gamma S L A: Gamma ⊢₊ S : L -> Gamma ⊢ linearize_terms S : (Arr (rev L) A) → A.
proof: Proof. intros H; econstructor; eapply AppR_typing with (L := L). eapply listtyping_preservation_under_renaming; [eassumption|..]. intros x ?; cbn; trivial. econstructor; trivial; simplify; cbn; intuition. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)