case mp p q _ prf₂ ih => exact BProof.mp ih prf₂
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
prf₂ : BTheorem (p⊃q)
ih : BProof {Form.conjoinList f l} p
⊢ BProof {Form.conjoinList f l} q
no goals