case mp P Q _ h₂ ih => 
  have ⟨fin, h₁, prf⟩ := ih
  exact ⟨fin, h₁, mp prf h₂⟩
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
no goals