case insert hd tl a1 ih =>
  simp at h1
  cases h1
  case inl c1 =>
    subst c1
    simp only [finset_var_name_max_len]
    simp
  case inr c1 =>
    simp only [finset_var_name_max_len] at ih
    simp only [finset_var_name_max_len]
    simp
    right
    exact ih c1
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x ∈ insert hd tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
no goals