simp only [isAlphaEqvVarList]
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] (hd :: tl) (hd :: tl)
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd ∧ isAlphaEqvVarList [] tl tl