have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
⊢ False
t : Th
f g : Form
h₁ : t⊨f⊃g
h₂ : ¬f⊃g ∈ ↑t
Δ : Th := { val := ▲{f}, property := (_ : ∀ {f_1 : Form}, f_1 ∈ ▲{f} ↔ ▲{f}⊢f_1) }
h₃ : g ∈ ↑(formalApplicationFunction t Δ)
q : Form
prf₁ : BProof {f} q
l₂ : q⊃g ∈ ↑t
prf₂ : BProof (↑t) (q⊃g)
prf₃ : BProof (↑t) (f⊃g)
⊢ False