have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
Γ : 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 ∈ Γ
⊢ False
Γ : 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)
⊢ False