obtain s1 := finset_var_name_max_len_mem x xs h
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length
x : VarName
c : Char
xs : Finset VarName
h : x ∈ xs
s1 : x.length ≤ finset_var_name_max_len xs
⊢ finset_var_name_max_len xs - x.length < finset_var_name_max_len xs + 1 - x.length