conv =>
  lhs; unfold mapMIdx; unfold mapMIdx.loop
  rw [dif_neg n.succ_ne_zero.symm]; dsimp
  rhs; ext b; change mapMIdx.loop f (cons a x) 1 n.zero_lt_succ (cons b empty)
  rw [mapMIdx.loop_cons_succ f a x 0 b empty]
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : Fin (n + 1) → α → m β
a : α
x : SizedArray α n
⊢ mapMIdx f (cons a x) = do
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ n) } a
    let y ← mapMIdx (f ∘ Fin.succ) x
    pure (cons b y)
no goals