case cons ys_hd ys_tl =>
  simp only [isAlphaEqvVarList] at h1
binders : List (VarName × VarName)
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVarList binders [] (ys_hd :: ys_tl)
⊢ [].length = (ys_hd :: ys_tl).length
no goals