simp only [Nat.ne_of_lt hlt, Nat.ne_of_lt (Nat.succ_lt_succ hlt), dif_neg]
case inr
α : 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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (if h : i + 1 = n + 1 then pure (h ▸ cons b r)
    else
      let_fun this := (_ : i + 1 < n + 1);
      do
      let __do_lift ← f { val := i + 1, isLt := this } (cons a x)[i + 1]
      let r : SizedArray β (i + 1 + 1) := push (cons b r) __do_lift
      loop f (cons a x) (i + 1 + 1) this r) =
    do
    let y ←
      if h : i = n then pure (h ▸ r)
        else
          let_fun this := (_ : i < n);
          do
          let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := this } x[i]
          let r : SizedArray β (i + 1) := push r __do_lift
          loop (f ∘ Fin.succ) x (i + 1) this r
    pure (cons b y)
case inr
α : 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
i : Nat
hi₁ : i + 1 ≤ n + 1
hi₂ : i ≤ n
b : β
r : SizedArray β i
hlt : i < n
⊢ (do
      let __do_lift ← f { val := i + 1, isLt := (_ : i + 1 < n + 1) } (cons a x)[i + 1]
      loop f (cons a x) (i + 1 + 1) (_ : i + 1 < n + 1) (push (cons b r) __do_lift)) =
    do
    let y ←
      do
        let __do_lift ← (f ∘ Fin.succ) { val := i, isLt := (_ : i < n) } x[i]
        loop (f ∘ Fin.succ) x (i + 1) (_ : i < n) (push r __do_lift)
    pure (cons b y)