proposition: Lemma AppR_typing_inv Gamma T B t: Gamma ⊢ AppR t T : B -> exists L, Gamma ⊢₊ T : L /\ Gamma ⊢ t : Arr (rev L) B.
proof: Proof. induction T in Gamma, B, t |-*; cbn; intros. - exists nil; intuition. - inv H. destruct (IHT _ _ _ H2) as [L]; intuition. exists (A :: L). intuition; cbn; rewrite Arr_app; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)