have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
Γ : 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
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
⊢ False
Γ : 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
h₄ : ~(P&Q) ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
l₂ : Q ∈ fun f => ¬~f ∈ Γ
prf₃ : BProof Γ (~P¦~Q)
l₃ : ~P ∈ Γ ∨ ~Q ∈ Γ
⊢ False