simp only [isAlphaEqvVarList] at h1
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ (xs_hd :: xs_tl).length = [].length
no goals