proposition: Lemma vars_ordertyping n x s A Gamma: x ∈ vars s -> Gamma ⊢(n) s : A -> exists B, nth Gamma x = Some B /\ ord B <= n.
proof: Proof. intros H % vars_varof; induction 1 in x, H |-*; inv H; eauto. eapply IHordertyping in H2 as []; eexists; eauto. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)