case cons ys_hd ys_tl =>
  simp only [isAlphaEqvVarList] at h2
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVarList binders [] (ys_hd :: ys_tl)
⊢ List.map V [] = List.map V' (ys_hd :: ys_tl)
no goals