case inl c1 =>
  subst c1
  simp only [finset_var_name_max_len]
  simp
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)
no goals