{ρ : Type} →
  {pat : ρ} →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      {σ : String.Slice → Type} →
        [inst_1 : String.Slice.Pattern.ToForwardSearcher pat σ] →
          [inst_2 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
            [inst_3 : ∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] →
              {motive : String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat → Sort u} →
                (t : String.Slice.Pattern.Model.LawfulToForwardSearcherModel pat) →
                  ((isValidSearchFrom_toList :
                        ∀ (s : String.Slice),
                          String.Slice.Pattern.Model.IsValidSearchFrom pat s.startPos
                            (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s).toList) →
                      motive ⋯) →
                    motive t