proposition: Lemma AppL_ordertyping_inv n Gamma T B t: Gamma ⊢(n) AppL T t : B -> exists L A, Gamma ⊢₊(n) T : L /\ Gamma ⊢(n) t : A.
proof: Proof. induction T in B |-*; cbn. - exists nil. exists B. intuition. - intros H; inv H. edestruct IHT as (? & ? & ?); (eauto 2). do 2 eexists; intuition; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)