cases ys
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys : List VarName
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) ys
⊢ List.map V (xs_hd :: xs_tl) = List.map V' ys
case nil
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ List.map V (xs_hd :: xs_tl) = List.map V' []

case cons
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
head✝ : VarName
tail✝ : List VarName
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) (head✝ :: tail✝)
⊢ List.map V (xs_hd :: xs_tl) = List.map V' (head✝ :: tail✝)