simp
x : VarName
tl : Finset VarName
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
a1 : x ∉ tl
⊢ x.length ≤ Finset.fold (fun m n => max m n) 0 (String.length ∘ VarName.toString) (insert x tl)
no goals