subst c1
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
c1 : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ finset_var_name_max_len (insert x tl)