induction prf₁
l : List Form
f g : Form
prf₁ : BProof { h | h = f ∨ h ∈ l } g
⊢ BProof {Form.conjoinList f l} g
case ax
l : List Form
f g p✝ : Form
h✝ : p✝ ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p✝

case mp
l : List Form
f g p✝ q✝ : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : BProof {Form.conjoinList f l} p✝
⊢ BProof {Form.conjoinList f l} q✝

case adj
l : List Form
f g p✝ q✝ : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p✝
h₂✝ : BProof { h | h = f ∨ h ∈ l } q✝
h₁_ih✝ : BProof {Form.conjoinList f l} p✝
h₂_ih✝ : BProof {Form.conjoinList f l} q✝
⊢ BProof {Form.conjoinList f l} (p✝&q✝)