rw [←l₂] at prf₂
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof {g} g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof (↑Gsing) g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g