cases h2
case left
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_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd
case left.intro
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_hd : VarName
ys_tl : List VarName
left✝ : isAlphaEqvVar binders xs_hd ys_hd
right✝ : isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd