dsimp at h
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : { index := index✝¹ }.index = { index := index✝ }.index
⊢ { index := index✝¹ } = { index := index✝ }
case mpr.mk.mk
index✝¹ index✝ : ℕ
h : index✝¹ = index✝
⊢ { index := index✝¹ } = { index := index✝ }