proposition: Lemma vars_ordertyping_nth n x s A B Gamma: x ∈ vars s -> Gamma ⊢(n) s : A -> nth Gamma x = Some B -> ord B <= n.
proof: Proof. intros; edestruct vars_ordertyping; eauto. intuition congruence. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)