case mp p q prf₁ prf₂ ih => 
  have l₁ := ih ⟨prf₁⟩
  have ⟨prf₃⟩ := Δ.property.mp l₁
  exact Δ.property.mpr ⟨BProof.mp prf₃ prf₂⟩
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
⊢ q ∈ ↑Δ
no goals