α : Type
d : ℕ
ds ds₁ ds₃ : List ℕ
a : Holor α ds₁
⊢ cast (_ : Holor α ds₁ = Holor α ds₁) a = fun t => a (cast (_ : HolorIndex ds₁ = HolorIndex ds₁) t)
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
⊢ cast (_ : Holor α ds₁ = Holor α ds₂) a = fun t => a (cast (_ : HolorIndex ds₂ = HolorIndex ds₁) t)
subst eq
no goals
α : Type
d : ℕ
ds ds₁ ds₃ : List ℕ
a : Holor α ds₁
⊢ cast (_ : Holor α ds₁ = Holor α ds₁) a = fun t => a (cast (_ : HolorIndex ds₁ = HolorIndex ds₁) t)
rfl