simp [init, Id.run, forIn', Std.Range.forIn']
α✝ : Type u_1
f : Fin 0 → α✝
⊢ init 0 f = #[]
α✝ : Type u_1
f : Fin 0 → α✝
⊢ Std.Range.forIn'.loop { start := 0, stop := 0, step := 1 }.start { start := 0, stop := 0, step := 1 }.stop 1
      (fun i h r => ForInStep.yield (push r (f { val := i, isLt := ⋯ }))) 0 0 ⋯ #[] =
    #[]