case adj p q prf₁ prf₂ ih₁ ih₂ => 
  have l₁ := ih₁ ⟨prf₁⟩
  have l₂ := ih₂ ⟨prf₂⟩
  have ⟨prf₃⟩ := Δ.property.mp l₁
  have ⟨prf₄⟩ := Δ.property.mp l₂
  exact Δ.property.mpr ⟨BProof.adj prf₃ prf₄⟩
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
⊢ p&q ∈ ↑Δ
no goals