cases h1
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h1 : x = hd ∨ x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)
case inl
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h✝ : x = hd
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)

case inr
x hd : VarName
tl : Finset VarName
a1 : hd ∉ tl
ih : x ∈ tl → x.length ≤ finset_var_name_max_len tl
h✝ : x ∈ tl
⊢ x.length ≤ finset_var_name_max_len (insert hd tl)