have l₂ := canonicalSatisfaction.mp h₃
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
⊢ f¦g ∈ p
t : Th
f g : Form
h₁ : t⊨f¦g
p : Set Form
h₂ : p ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
pr : Pr :=
  { val := { val := p, property := (_ : ∀ {f : Form}, f ∈ p ↔ p⊢f) },
    property := (_ : ∀ {f g : Form}, f¦g ∈ p → f ∈ p ∨ g ∈ p) }
h₃ : ↑pr⊨f
l₂ : f ∈ ↑↑pr
⊢ f¦g ∈ p