cases v₂
case mpr.mk
v₂ : Variable
index✝ : ℕ
h : { index := index✝ }.index = v₂.index
⊢ { index := index✝ } = v₂
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : { index := index✝¹ }.index = { index := index✝ }.index
⊢ { index := index✝¹ } = { index := index✝ }