exact IH (j+1) _ (push y b)
case succ.h
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type v
a : α
x : Array α
f : Fin (size x + 1) → α → m β
i : Nat
IH :
  ∀ (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
j : Nat
h : Nat.succ i + (j + 1) = size x + 1
y : Array β
b : β
⊢ map (cons a x) f i (j + 1 + 1) (_ : i + (j + 1 + 1) = Nat.succ (size x)) (push y b) =
    map x (f ∘ Fin.succ) i (j + 1) (_ : i + (j + 1) = size x) (push y b)
no goals