have l₁ : ↑s₁ ⊆ {h : Form | h = f ∨ h ∈ lst₁} := by
  intros k h₂
  cases decEq f k
  case isTrue h₃ => rw [h₃]; exact Or.inl rfl
  case isFalse h₃ => 
    have l₂ : k ∈ lst₁ := by
      apply Finset.mem_toList.mpr
      exact Finset.mem_erase.mpr ⟨h₃ ∘ Eq.symm, h₂⟩
    exact Or.inr l₂
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g
Γ : Ctx
f g : Form
h₁ : BProof (insert f Γ) g
s₁ : Finset Form
h₂ : ↑s₁ ⊆ insert f Γ
prf₁ : BProof (↑s₁) g
lst₁ : List Form := Finset.toList (Finset.erase s₁ f)
l₁ : ↑s₁ ⊆ { h | h = f ∨ h ∈ lst₁ }
⊢ (l : List Form) × (_ : { x | x ∈ l } ⊆ Γ) ×' BProof {Form.conjoinList f l} g