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