case or.mp f g =>
  rw [primeAnalysis]
  intros p h₂
  let pr : Pr := ⟨⟨p, h₂.right.right⟩,h₂.left⟩
  have l₁ := @h₁ pr h₂.right.left
  cases l₁
  case inl h₃ => 
    have l₂ := canonicalSatisfaction.mp h₃
    exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₁⟩
  case inr h₃ => 
    have l₂ := canonicalSatisfaction.mp h₃
    exact h₂.right.right.mpr ⟨BProof.mp (BProof.ax l₂) BTheorem.orI₂⟩
t : Th
f g : Form
h₁ : t⊨f¦g
⊢ f¦g ∈ ↑t
no goals