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