{α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      {motive : Std.Rxo.IsAlwaysFinite α → Sort u_1} →
        (t : Std.Rxo.IsAlwaysFinite α) →
          ((finite : ∀ (init hi : α), ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x < hi) → motive ⋯) →
            motive t