case mpr =>
  intros h₁  
  have ⟨w⟩ := h₁
  induction w
  case ax => assumption
  case mp P Q prf thm ih => 
    have ⟨prf₂⟩ := ih ⟨prf⟩
    exact ⟨BProof.mp prf₂ thm⟩
  case adj P Q prf₁ prf₂ ih₁ ih₂ => 
    have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
    have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
    exact ⟨BProof.adj prf₃ prf₄⟩
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ
no goals