constructor
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd ∧ isAlphaEqvVarList [] tl tl
case left
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd

case right
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] tl tl