{G : Type u} →
  {motive : LeftCancelSemigroup G → Sort u_1} →
    ([toSemigroup : Semigroup G] →
        [toIsLeftCancelMul : IsLeftCancelMul G] →
          motive { toSemigroup := toSemigroup, toIsLeftCancelMul := toIsLeftCancelMul }) →
      (t : LeftCancelSemigroup G) → motive t