no goals
ι : Type u
α : ι → Type v
i✝ j : ι
l : List ι
f : (i : ι) → α i
inst✝ : DecidableEq ι
hnd : Nodup l
h : ∀ (i : ι), i ∈ l
v : TProd α l
i : ι
hi : i ∈ l
⊢ TProd.elim (TProd.mk l (TProd.elim' h v)) hi = TProd.elim v hi
simp [elim_mk]