induction prf
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
prf : BProof Γ f
⊢ f ∈ ↑Δ
case ax
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ : Form
h✝ : p✝ ∈ Γ
h₂ : p✝ ∈ ▲Γ
⊢ p✝ ∈ ↑Δ

case mp
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : p✝ ∈ ▲Γ → p✝ ∈ ↑Δ
h₂ : q✝ ∈ ▲Γ
⊢ q✝ ∈ ↑Δ

case adj
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BProof Γ q✝
h₁_ih✝ : p✝ ∈ ▲Γ → p✝ ∈ ↑Δ
h₂_ih✝ : q✝ ∈ ▲Γ → q✝ ∈ ↑Δ
h₂ : p✝&q✝ ∈ ▲Γ
⊢ p✝&q✝ ∈ ↑Δ