case adj P Q prf₁ prf₂ ih₁ ih₂ =>
  intros h₄
  have l₁ := ih₁ ⟨prf₁⟩
  have l₂ := ih₂ ⟨prf₂⟩
  have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
  have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
  cases l₃
  case inl left => exact l₁ left
  case inr right => exact l₂ right
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₁ : BProof (FormalDual Γ) P
prf₂ : BProof (FormalDual Γ) Q
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
ih₂ : FormalDual Γ⊢Q → Q ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢P&Q
⊢ P&Q ∈ fun f => ¬~f ∈ Γ
no goals