case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp only [isAlphaEqvVarList] at h1
  case cons ys_hd ys_tl =>
    simp only [isAlphaEqvVarList] at h1
    simp
    cases h1
    case intro h1_left h1_right =>
      exact xs_ih ys_tl h1_right
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
ys : List VarName
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) ys
⊢ (xs_hd :: xs_tl).length = ys.length
no goals