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
c1 : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
no goals