English
For any α and i, read that ofRepeat (α.repeatEq i (prod.mk i x y)) is equivalent to x = y; i.e., equality of the two components in the product is captured by the repeat equality predicate.
Русский
Для любого α и i, справедливо, что ofRepeat (α.repeatEq i (prod.mk i x y)) эквивалентно x = y; тождество двух компонент в произведении задается повторяющимся предикатом равенства.
LaTeX
$$$\\operatorname{ofRepeat}( \\alpha.\\text{repeatEq}\\ i\\ (\\mathrm{prod.mk}\\ i\\ x\\ y) ) \\iff x = y$$$
Lean4
theorem repeatEq_iff_eq {α : TypeVec n} {i x y} : ofRepeat (repeatEq α i (prod.mk _ x y)) ↔ x = y := by
induction i with
| fz => rfl
| fs _ i_ih =>
rw [repeatEq]
exact i_ih
