∀ (base x x_1 : ℕ) (x_2 : List Char),
  base.toDigitsCore x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, ds => ds
    | fuel.succ, n, ds =>
      have d := (n % base).digitChar;
      have n' := n / base;
      if n' = 0 then d :: ds else base.toDigitsCore fuel n' (d :: ds)