∀ (s : String.Slice)
  (motive :
    Std.IterStep (Std.IterM Id (String.Slice.Pattern.SearchStep s)) (String.Slice.Pattern.SearchStep s) → Sort u_1)
  (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
      (out : String.Slice.Pattern.SearchStep s) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM Id (String.Slice.Pattern.SearchStep s)) → motive (Std.IterStep.skip it'))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'