rw [dif_pos rfl]
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ (if h : 0 = 0 then pure (h ▸ mkEmpty 0)
    else
      let_fun this := (_ : 0 < 0);
      do
      let __do_lift ← f { val := 0, isLt := this } empty[0]
      let r : SizedArray β (0 + 1) := push (mkEmpty 0) __do_lift
      mapMIdx.loop f empty (0 + 1) this r) =
    pure empty
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝ : Monad m
f : Fin 0 → α → m β
⊢ pure ((_ : 0 = 0) ▸ mkEmpty 0) = pure empty