{ρ : Type} →
  {pat : ρ} →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} →
        {startPos endPos : s.Pos} →
          {motive : String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos → Sort u} →
            ((le : startPos ≤ endPos) →
                (isLongestRevMatch_sliceTo :
                    String.Slice.Pattern.Model.IsLongestRevMatch pat (endPos.sliceTo startPos le)) →
                  motive ⋯) →
              (t : String.Slice.Pattern.Model.IsLongestRevMatchAt pat startPos endPos) → motive t