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