have l₁ := ih ⟨prf₁⟩
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
⊢ q ∈ ↑Δ
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ q ∈ ↑Δ