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