have l₂ : Gsing = ({g} : Ctx) := Finset.coe_singleton g
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : 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}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g