simp [if_neg h]
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ (if x ∈ xs then fresh { toString := x.toString ++ c.toString } c xs else x) ∉ xs
x : VarName
c : Char
xs : Finset VarName
h : x ∉ xs
⊢ x ∉ xs