induction xs
xs : List VarName
⊢ isAlphaEqvVarList [] xs xs
case nil

⊢ isAlphaEqvVarList [] [] []

case cons
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isAlphaEqvVarList [] tail✝ tail✝
⊢ isAlphaEqvVarList [] (head✝ :: tail✝) (head✝ :: tail✝)