proposition: Lemma AppL_typing_inv Gamma T B t: Gamma ⊢ AppL T t : B -> exists L A, Gamma ⊢₊ T : L /\ Gamma ⊢ 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)