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