proposition: Lemma typing_variables Gamma s A: Gamma ⊢ s : A -> forall x, x ∈ vars s -> x ∈ dom Gamma.
proof: Proof. intros ? x H1 % vars_varof. induction H in x, H1 |-*; inv H1; eauto. - now domin H. - specialize (IHtyping _ H2). eapply dom_lt_iff in IHtyping. cbn in *. assert (x < length Gamma) by lia. auto. Qed.
imports: List Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics)