induction prf₁
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
prf₁ : BProof (FormalDual Γ) F
⊢ F ∈ fun f => ¬~f ∈ Γ
case ax
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ : Form
h✝ : p✝ ∈ FormalDual Γ
h₃ : FormalDual Γ⊢p✝
⊢ p✝ ∈ fun f => ¬~f ∈ Γ

case mp
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ q✝ : Form
h₁✝ : BProof (FormalDual Γ) p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : FormalDual Γ⊢p✝ → p✝ ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢q✝
⊢ q✝ ∈ fun f => ¬~f ∈ Γ

case adj
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F p✝ q✝ : Form
h₁✝ : BProof (FormalDual Γ) p✝
h₂✝ : BProof (FormalDual Γ) q✝
h₁_ih✝ : FormalDual Γ⊢p✝ → p✝ ∈ fun f => ¬~f ∈ Γ
h₂_ih✝ : FormalDual Γ⊢q✝ → q✝ ∈ fun f => ¬~f ∈ Γ
h₃ : FormalDual Γ⊢p✝&q✝
⊢ p✝&q✝ ∈ fun f => ¬~f ∈ Γ