proposition: Lemma Vars_listordertyping x n Gamma S L: Gamma ⊢₊(n) S : L -> x ∈ Vars S -> exists A, nth Gamma x = Some A /\ ord A <= n.
proof: Proof. induction 1; cbn; simplify; intuition eauto using vars_ordertyping. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)