rw [dif_neg (n+1).lt_irrefl]
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ (if h : n + 1 < n + 1 then
      ofFn.go f (n + 1 + 1)
        (push (push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) (f { val := n + 1, isLt := h }))
    else push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1)
            (push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f { val := ↑{ val := n + 1, isLt := h_1 }, isLt := (_ : ↑{ val := n + 1, isLt := h_1 } < Nat.succ n) }))
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ push acc (f { val := n, isLt := (_ : n < Nat.succ n) }) =
    push
      (if h : n < n then
        if h_1 : n + 1 < n then
          ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1 + 1)
            (push
              (push acc
                (f
                  { val := ↑{ val := n, isLt := (_ : n < n) },
                    isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) }))
              (f { val := ↑{ val := n + 1, isLt := h_1 }, isLt := (_ : ↑{ val := n + 1, isLt := h_1 } < Nat.succ n) }))
        else
          push acc
            (f
              { val := ↑{ val := n, isLt := (_ : n < n) },
                isLt := (_ : ↑{ val := n, isLt := (_ : n < n) } < Nat.succ n) })
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })