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