(motive : DoResultSBC (List Lean.MVarId × Lean.PersistentArray Lean.Elab.InfoTree) PUnit.{1} → Sort u_1) →
  (r : DoResultSBC (List Lean.MVarId × Lean.PersistentArray Lean.Elab.InfoTree) PUnit.{1}) →
    ((a : List Lean.MVarId × Lean.PersistentArray Lean.Elab.InfoTree) →
        (u : PUnit.{1}) → motive (DoResultSBC.pureReturn a u)) →
      ((u : PUnit.{1}) → motive (DoResultSBC.break u)) → ((u : PUnit.{1}) → motive (DoResultSBC.continue u)) → motive r