induction prf₁
Γ : Ctx
f : Form
prf₁ : BProof Γ f
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f
case ax
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝

case mp
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) q✝

case adj
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BProof Γ q✝
h₁_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝
h₂_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) q✝
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (p✝&q✝)