rw [dif_neg (c:=0=0+1) (by decide), dif_pos rfl]
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (if h : 0 = 0 + 1 then pure (h ▸ mkEmpty (0 + 1))
    else
      let_fun this := (_ : 0 < 0 + 1);
      do
      let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
      mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ←
      if h : 0 = 0 then pure (h ▸ mkEmpty 0)
        else
          let_fun this := (_ : 0 < 0);
          do
          let __do_lift ←
            f { val := ↑{ val := 0, isLt := this }, isLt := (_ : ↑{ val := 0, isLt := this } < Nat.succ 0) } empty[0]
          let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
          mapMIdx.loop (fun i => f { val := ↑i, isLt := (_ : ↑i < Nat.succ 0) }) empty (0 + 1) this r
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f✝ : Fin (n + 1) → α → m β
x : SizedArray α n
a : α
f : Fin (0 + 1) → α → m β
⊢ (let_fun this := (_ : 0 < 0 + 1);
    do
    let __do_lift ← f { val := 0, isLt := this } (push empty a)[0]
    let r : SizedArray β (0 + 1) := push (mkEmpty (0 + 1)) __do_lift
    mapMIdx.loop f (push empty a) (0 + 1) this r) =
    do
    let y ← pure ((_ : 0 = 0) ▸ mkEmpty 0)
    let b ← f { val := 0, isLt := (_ : 0 < Nat.succ 0) } a
    pure (push y b)