(motive : String.Pos.Raw × String.Pos.Raw × String.Pos.Raw → Sort u_1) →
  (x : String.Pos.Raw × String.Pos.Raw × String.Pos.Raw) →
    ((start stopTk stopWs : String.Pos.Raw) → motive (start, stopTk, stopWs)) → motive x