{s : String.Slice} →
  (motive : List (String.Slice.Pattern.SearchStep s) → Sort u_1) →
    (l : List (String.Slice.Pattern.SearchStep s)) →
      (Unit → motive []) →
        ((startPos endPos : s.Pos) →
            (l : List (String.Slice.Pattern.SearchStep s)) →
              motive (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l)) →
          ((p q : s.Pos) →
              (l : List (String.Slice.Pattern.SearchStep s)) →
                motive (String.Slice.Pattern.SearchStep.matched p q :: l)) →
            motive l