English
If two index lists ds1 and ds2 are equal, then every Holor α ds1 corresponds to a Holor α ds2 via a canonical transport along the equality; concretely, cast (congr_arg Holor α eq) a reindexes a Holor a of ds1 to ds2.
Русский
Если два списка индексов ds1 и ds2 равны, то каждый Holor α ds1 можно транспонировать к Holor α ds2 по каноническому переносу вдоль равенства; явно cast (congr_arg Holor α eq) a переиндексирует Holor a из ds1 в ds2.
LaTeX
$$$\forall {\alpha : Type} {ds_1 ds_2 : List\,Nat} (eq : ds_1 = ds_2) (a : Holor\, \alpha\, ds_1),\ cast (congr_arg (Holor\, \alpha) eq)\ a = \lambda t. a (cast (congr_arg HolorIndex eq.symm) t)$$$
Lean4
theorem cast_type (eq : ds₁ = ds₂) (a : Holor α ds₁) :
cast (congr_arg (Holor α) eq) a = fun t => a (cast (congr_arg HolorIndex eq.symm) t) := by subst eq; rfl
