contradiction
L : Language
Δ✝ Δ₁ Δ₂ Γ : Sequent L
p✝ q r : SyntacticFormula L
Δ : Sequent L
p : Semiformula L ℕ 0
hp : p ∈ Δ
x : ℕ
hx : p.fvar? x
h : ∀ p ∈ Δ, ¬fvar? p x
this : ¬p.fvar? x
⊢ False
no goals