simp only [isAlphaEqvVar] at h2
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : isAlphaEqvVar [] x y
⊢ h1_V x = h1_V y
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' h1_V : VarAssignment D
h2 : x = y
⊢ h1_V x = h1_V y