{G : Type u} →
  [inst : Add G] →
    {motive : IsCancelAdd G → Sort u_1} →
      ([toIsLeftCancelAdd : IsLeftCancelAdd G] → [toIsRightCancelAdd : IsRightCancelAdd G] → motive ⋯) →
        (t : IsCancelAdd G) → motive t