rintro rfl
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
m : ℕ
p : SyntacticSemiformula L 1
h : ¬fvar? p m
x : ℕ
hx : fvar? p x
⊢ ¬x = m
L : Language
Δ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
p : SyntacticSemiformula L 1
x : ℕ
hx : fvar? p x
h : ¬fvar? p x
⊢ False