cases h2_left
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_left : ¬x = h1_x ∧ ¬y = h1_y
h2_right : isAlphaEqvVar h1_l x y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
case intro
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_right : isAlphaEqvVar h1_l x y
left✝ : ¬x = h1_x
right✝ : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y