induction h1
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVar binders x y
⊢ V x = V' y
case nil
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' V✝ : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ V✝ x = V✝ y

case cons
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
binders✝ : List (VarName × VarName)
x✝ y✝ : VarName
V✝ V'✝ : VarAssignment D
d✝ : D
a✝ : AlphaEqvVarAssignment D binders✝ V✝ V'✝
a_ih✝ : isAlphaEqvVar binders✝ x y → V✝ x = V'✝ y
h2 : isAlphaEqvVar ((x✝, y✝) :: binders✝) x y
⊢ Function.updateITE V✝ x✝ d✝ x = Function.updateITE V'✝ y✝ d✝ y