exact l₁ $ canonicalSatisfaction.mp (h₁ l₂)
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 Δ)
l₂ : Δ⊨f
⊢ False
no goals