if h':i=j then simp [h'] at h else simp[h']
X : Sort u_3
I : Sort u_1
XI : I → Type u_2
inst✝² : StructType X I XI
inst✝¹ : DecidableEq I
inst✝ : (i : I) → Zero (XI i)
i j : I
xi : XI i
h : i ≠ j
⊢ ∀ (h : i = j), h ▸ xi = 0
no goals