exact Finset.mem_erase.mpr ⟨h₃ ∘ Eq.symm, h₂⟩
Γ : 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)
k : Form
h₂ : k ∈ ↑s₁
h₃ : ¬f = k
⊢ k ∈ Finset.erase s₁ f
no goals