case adj P Q prf₁ prf₂ ih₁ ih₂ => 
  have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
  have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
  exact ⟨BProof.adj prf₃ prf₄⟩
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
⊢ P&Q ∈ ▲Γ
no goals