proposition: Lemma var_typing n Gamma: ord' Gamma <= n -> Gamma ⊩(n) @var X : Gamma.
proof: Proof. intros ????; econstructor; (eauto 1); eapply ord'_elements; eauto using nth_error_In. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)