show mapIdxM.map (cons a x) f x.size 1 rfl #[b] = _
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map { data := a :: x.data } f (Nat.add (List.length x.data) 0) (0 + 1)
      (_ : Nat.add (List.length x.data) 0 + (0 + 1) = size { data := a :: x.data }) (push #[] b) =
    do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)
case h
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
a : α
x : Array α
f : Fin (size x + 1) → α → m β
b : β
⊢ mapIdxM.map (cons a x) f (size x) 1 (_ : size x + 1 = size x + 1) #[b] = do
    let y ← mapIdxM.map x (f ∘ Fin.succ) (size x) 0 (_ : size x + 0 = size x + 0) (mkEmpty (size x))
    pure (cons b y)