∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos}
  {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidSearchFrom p pos l =
    String.Slice.Pattern.Model.IsValidSearchFrom (fun x => decide (p x)) pos l