rw [dif_neg (Nat.lt_irrefl n.succ), dif_neg (Nat.lt_irrefl n)]
case refine_1
α✝ α : Type u
n : Nat
f : Fin (Nat.succ n) → α
i : Nat
acc✝ : Array α
hlt : i < n
acc : Array α
⊢ (if h : Nat.succ n < Nat.succ n then ofFn.go f (Nat.succ n + 1) (push acc (f { val := Nat.succ n, isLt := h }))
    else acc) =
    if h : n < n then ofFn.go (f ∘ Fin.succ) (n + 1) (push acc ((f ∘ Fin.succ) { val := n, isLt := h })) else acc
no goals