case nil h1_V =>
  simp only [isAlphaEqvVar] at h2
  subst h2
  rfl
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
no goals