intro hm
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
⊢ m ∉ fvarList p
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : (fvarList p).toFinset.sup id < m
hm : m ∈ fvarList p
⊢ False