rw [dif_pos n.lt_succ_self]
case refl
α : Type u
n : Nat
f : Fin (n + 1) → α
acc : Array α
H : n < n + 1
⊢ (if h : n < n + 1 then ofFn.go f (n + 1) (push acc (f { val := n, isLt := h })) else acc) =
    push
      (if h : n < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1)
          (push acc (f { val := ↑{ val := n, isLt := h }, isLt := (_ : ↑{ val := n, isLt := h } < 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
⊢ ofFn.go f (n + 1) (push acc (f { val := n, isLt := (_ : n < Nat.succ n) })) =
    push
      (if h : n < n then
        ofFn.go (fun x => f { val := ↑x, isLt := (_ : ↑x < Nat.succ n) }) (n + 1)
          (push acc (f { val := ↑{ val := n, isLt := h }, isLt := (_ : ↑{ val := n, isLt := h } < Nat.succ n) }))
      else acc)
      (f { val := n, isLt := (_ : n < Nat.succ n) })