case adj P Q _ _ ih₁ ih₂ => 
  have ⟨fin₁, h₁, prf₁⟩ := ih₁
  have ⟨fin₂, h₂, prf₂⟩ := ih₂
  have prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P := BProof.monotone (Set.subset_union_left ↑fin₁ ↑fin₂) prf₁
  have prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q := BProof.monotone (Set.subset_union_right ↑fin₁ ↑fin₂) prf₂
  have prf₅ := adj prf₃ prf₄
  have l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ := by
    intros f h₃
    rw [Finset.coe_union] at h₃
    cases h₃
    case inl h₄ => exact h₁ h₄
    case inr h₄ => exact h₂ h₄
  rw [←Finset.coe_union] at prf₅
  exact ⟨↑(fin₁ ∪ fin₂), l₁, prf₅⟩
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
no goals