proposition: Lemma orderlisttyping_app n Gamma S1 S2 L1 L2: Gamma ⊢₊(n) S1 : L1 -> Gamma ⊢₊(n) S2 : L2 -> Gamma ⊢₊(n) S1 ++ S2 : L1 ++ L2.
proof: Proof. induction 1; cbn; (eauto 3). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)