English
If i ≍ j is a heterogeneous equality between Fin indices, then i.val = j.val.
Русский
Если i ≍ j — гетерогенная эквивалентность между индексами Fin, то i.val = j.val.
LaTeX
$$$\forall {k\ell}, \; {i : \mathrm{Fin}(k)}, {j : \mathrm{Fin}(\ell)}, (i \equiv\!\!\! j) \Rightarrow i.\mathrm{val} = j.\mathrm{val}$$$
Lean4
theorem val_eq_val_of_heq {k l : ℕ} {i : Fin k} {j : Fin l} (h : i ≍ j) : (i : ℕ) = (j : ℕ) :=
(Fin.heq_ext_iff (fin_injective (type_eq_of_heq h))).1 h