Int64.instUpwardEnumerable =
  { succ? := fun i => if i + 1 = Int64.minValueSealed✝ then none else some (i + 1),
    succMany? := fun n i =>
      have this := ⋯;
      if h : i.toInt + ↑n ≤ Int64.maxValueSealed✝.toInt then some (Int64.ofIntLE (i.toInt + ↑n) ⋯ ⋯) else none }