have l₁ : ¬(g ∈ (formalApplicationFunction t Δ).val) := by
  intros h₃
  have ⟨q,⟨prf₁⟩,l₂⟩ := h₃
  have ⟨prf₂⟩ := t.property.mp l₂
  have prf₃ := BProof.mp prf₂ (BTheorem.hs prf₁.toTheorem BTheorem.taut)
  exact h₂ $ t.property.mpr ⟨prf₃⟩
case h
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) }
⊢ False
case h
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) }
l₁ : ¬g ∈ ↑(formalApplicationFunction t Δ)
⊢ False