{G : Type u_9} →
  {P : Type u_10} →
    [inst : SMul G P] →
      {motive : IsCancelSMul G P → Sort u} →
        (t : IsCancelSMul G P) →
          ([toIsLeftCancelSMul : IsLeftCancelSMul G P] →
              (right_cancel' : ∀ (a b : G) (c : P), a • c = b • c → a = b) → motive ⋯) →
            motive t