exact ⟨BTheorem.adj l₁ l₂⟩
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
l₂ : BTheorem Q
⊢ P&Q ∈ BTheory
no goals