simp
α✝ : Type u_1
f : Fin 0 → α✝
⊢ (if hu : 0 < { start := 0, stop := 0, step := 1 }.stop then
      match 0 with
      | 0 => pure #[]
      | Nat.succ fuel => do
        let __do_lift ← ForInStep.yield (push #[] (f { val := 0, isLt := ⋯ }))
        match __do_lift with
          | ForInStep.done b => pure b
          | ForInStep.yield b =>
            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 := ⋯ }))) fuel (0 + 1) ⋯ b
    else pure #[]) =
    #[]
no goals