intros h₄
Γ : 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 ∈ Γ
Γ : 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) ∈ Γ
⊢ False