case cons h1_l h1_x h1_y h1_V h1_V' h1_d _ h1_ih =>
  simp only [isAlphaEqvVar] at h2
  simp only [Function.updateITE]
  cases h2
  case inl h2 =>
    cases h2
    case intro h2_left h2_right =>
      simp only [if_pos h2_left, if_pos h2_right]
  case inr h2 =>
    cases h2
    case intro h2_left h2_right =>
      cases h2_left
      case intro h2_left_left h2_left_right =>
        simp only [if_neg h2_left_left, if_neg h2_left_right]
        exact h1_ih h2_right
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2 : isAlphaEqvVar ((h1_x, h1_y) :: h1_l) x y
⊢ Function.updateITE h1_V h1_x h1_d x = Function.updateITE h1_V' h1_y h1_d y
no goals