simp only [dif_neg (Nat.ne_of_lt this), dif_neg (Nat.ne_of_lt (Nat.succ_lt_succ this))]
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ b)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) this __do_lift) =
    if h : i = n then pure (h ▸ b)
    else
      let_fun this := (_ : i < n);
      do
      let __do_lift ← f (i + 1) b x[i]
      loop (fun i b => f (i + 1) b) x (i + 1) this __do_lift
α : Type u
β✝ : Type v
n : Nat
β : Nat → Type v
m : Type v → Type w
inst✝ : Monad m
f : (i : Nat) → β i → α → m (β (i + 1))
a : α
x : SizedArray α n
i : Nat
h₁ : i + 1 ≤ n + 1
h₂ : i ≤ n
b : β (i + 1)
h : ¬i = n
this : i < n
⊢ (do
      let __do_lift ← f (i + 1) b (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) __do_lift) =
    do
    let __do_lift ← f (i + 1) b x[i]
    loop (fun i b => f (i + 1) b) x (i + 1) (_ : i < n) __do_lift