induction i generalizing j y with
| zero => dsimp [map]
| succ i IH =>
  unfold map; dsimp
  apply bind_congr; intro b
  exact IH (j+1) _ (push y b)
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i j : Nat
h : i + (j + 1) = size x + 1
y : Array β
⊢ map (cons a x) f i (j + 1) h y = map x (f ∘ Fin.succ) i j (_ : i + j = size x) y
no goals