case or.mpr f g =>
  intros p h₂
  rw [primeAnalysis] at h₁
  have l₁ : f ¦ g ∈ p.val.val := (Set.mem_interₛ.mp h₁ p) ⟨p.property, h₂, p.val.property⟩
  have l₂ : f ∈ p.val.val ∨ g ∈ p.val.val := p.property l₁
  cases l₂
  case inl h₂ => exact Or.inl $ canonicalSatisfaction.mpr h₂
  case inr h₂ => exact Or.inr $ canonicalSatisfaction.mpr h₂
t : Th
f g : Form
h₁ : f¦g ∈ ↑t
⊢ t⊨f¦g
no goals