suffices ∀ i (hi : i ≤ n) o (_ : o.size = n-i),
  Std.Range.forIn'.loop (m := Id) 0 n.succ 1
    (fun i h r => ForInStep.yield (push r (f ⟨i, h.2⟩)))
    i.succ (n-i)
    (Nat.zero_le _)
    o
  = push (Std.Range.forIn'.loop (m := Id) 0 n 1
    (fun i h r => ForInStep.yield (push r (f ⟨i, Nat.le_step h.2⟩)))
    i (n-i)
    (Nat.zero_le _)
    o) (f ⟨n, Nat.lt_succ_self n⟩)
  by
  have := this n (Nat.le_refl _) #[] (by simp)
  simp at this
  exact this
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ Std.Range.forIn'.loop { start := 0, stop := Nat.succ n, step := 1 }.start
      { start := 0, stop := Nat.succ n, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) (Nat.succ n) 0 ⋯ #[] =
    push
      (Std.Range.forIn'.loop { start := 0, stop := n, step := 1 }.start { start := 0, stop := n, step := 1 }.stop 1
        (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) n 0 ⋯ #[])
      (f { val := n, isLt := ⋯ })
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ ∀ (i : Nat),
    i ≤ n →
      ∀ (o : Array α),
        size o = n - i →
          Std.Range.forIn'.loop 0 (Nat.succ n) 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ })))
              (Nat.succ i) (n - i) ⋯ o =
            push
              (Std.Range.forIn'.loop 0 n 1 (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) i (n - i)
                ⋯ o)
              (f { val := n, isLt := ⋯ })