proposition: Lemma Vars_listtyping x Gamma S L: Gamma ⊢₊ S : L -> x ∈ Vars S -> x ∈ dom Gamma.
proof: Proof. induction 1; cbn; simplify; intuition eauto using typing_variables. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)