apply Fin.val_eq_val_of_heq
case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.set i (as.get j)).size = as.size

case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j