case mpr =>
  have ⟨prf₁⟩ := h₃
  induction prf₁
  case ax => assumption
  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₂⟩) 
  case adj P Q prf₁ prf₂ ih₁ ih₂ =>
    intros h₄
    have l₁ := ih₁ ⟨prf₁⟩
    have l₂ := ih₂ ⟨prf₂⟩
    have prf₃ := BProof.mp (BProof.ax h₄) BTheorem.demorgansLaw3
    have l₃ := h₂ (h₁.mpr ⟨prf₃⟩)
    cases l₃
    case inl left => exact l₁ left
    case inr right => exact l₂ right
Γ : Ctx
h₁ : formalTheory Γ
h₂ : isPrimeTheory Γ
F : Form
h₃ : FormalDual Γ⊢F
⊢ F ∈ fun f => ¬~f ∈ Γ
no goals