have prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q := BProof.monotone (Set.subset_union_right ↑fin₁ ↑fin₂) 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
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Γ : 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
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)