case impl.mp f g =>
  apply byContradiction
  intros h₂
  let Δ : Th := ⟨▲{f}, generatedFormal {f}⟩
  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₃⟩
  have l₂ : Δ ⊨ f := canonicalSatisfaction.mpr ⟨BProof.ax rfl⟩
  exact l₁ $ canonicalSatisfaction.mp (h₁ l₂)
t : Th
f g : Form
h₁ : t⊨f⊃g
⊢ f⊃g ∈ ↑t
no goals