induction xs generalizing ys
D : Type
binders : List (VarName × VarName)
xs ys : List VarName
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVarList binders xs ys
⊢ List.map V xs = List.map V' ys
case nil
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2 : isAlphaEqvVarList binders [] ys
⊢ List.map V [] = List.map V' ys

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