{α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : Std.Rxi.HasSize α] →
      {motive : Std.Rxi.LawfulHasSize α → Sort u_1} →
        (t : Std.Rxi.LawfulHasSize α) →
          ((size_eq_one_of_succ?_eq_none : ∀ (lo : α), Std.PRange.succ? lo = none → Std.Rxi.HasSize.size lo = 1) →
              (size_eq_succ_of_succ?_eq_some :
                  ∀ (lo lo' : α),
                    Std.PRange.succ? lo = some lo' → Std.Rxi.HasSize.size lo = Std.Rxi.HasSize.size lo' + 1) →
                motive ⋯) →
            motive t