simp [init, Id.run, forIn', Std.Range.forIn']
α : Type u_1
n : Nat
f : Fin (Nat.succ n) → α
⊢ init (Nat.succ n) f = push (init n fun i => f { val := ↑i, isLt := ⋯ }) (f { val := n, isLt := ⋯ })
α : 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 := ⋯ })