case mp P Q prf₂ thm₁ ih₁ =>
  intros h₄
  have l₁ := ih₁ ⟨prf₂⟩
  unfold FormalDual at l₁
  have thm₂ : BTheorem (~Q ⊃ ~P) := BTheorem.cp $ BTheorem.transitivity thm₁ (BTheorem.cp BTheorem.taut)
  have prf₂ := BProof.mp (BProof.ax h₄) thm₂
  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
⊢ Q ∈ fun f => ¬~f ∈ Γ
no goals