rw [mapIdx_cons]
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (mapIdx (cons a x) f) = size (cons a x)
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
x✝ : Array α
f✝ : Fin (size x✝) → α → β
a : α
x : Array α
IH : ∀ (x_1 : Fin (size x) → α → β), size (mapIdx x x_1) = size x
f : Fin (size (cons a x)) → α → β
⊢ size (cons (f { val := 0, isLt := (_ : 0 < Nat.succ (size x)) } a) (mapIdx x (f ∘ Fin.succ))) = size (cons a x)