proposition: Lemma AppR_ordertyping n Gamma T s L B: Gamma ⊢₊(n) T : L -> Gamma ⊢(n) s : Arr (rev L) B -> Gamma ⊢(n) AppR s T : B.
proof: Proof. induction 1 in s, B |-*; cbn; (eauto 1); rewrite Arr_app; 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)