{m : Type u_1 → Type u_2} →
  {motive : AlternativeMonad m → Sort u} →
    (t : AlternativeMonad m) →
      ([toAlternative : Alternative m] →
          [toBind : Bind m] → motive { toAlternative := toAlternative, toBind := toBind }) →
        motive t