simp[upper, Nat.add_one_le_iff, fvar?] at h ⊢
L : Language
ξ : Type u_1
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
p : SyntacticSemiformula L n
h : upper p ≤ m
⊢ ¬fvar? p m
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