exact l₁ (h₁.mpr ⟨prf₂⟩)
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F P Q : Form
prf₂✝ : BProof (FormalDual Γ) P
thm₁ : BTheorem (P⊃Q)
ih₁ : FormalDual Γ⊢P → P ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢Q
h₄ : ~Q ∈ Γ
l₁ : P ∈ fun f => ¬~f ∈ Γ
thm₂ : BTheorem (~Q⊃~P)
prf₂ : BProof Γ ~P
⊢ False
no goals