dsimp [map]
case zero
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
j : Nat
h : Nat.zero + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f Nat.zero (j + 1) h y = map x (f ∘ Fin.succ) Nat.zero j (_ : Nat.zero + j = size x) y
no goals