no goals
l m r : List Char
f : Char → Bool
⊢ Substring.any
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } }
      f =
    List.any m f
simp [-List.append_assoc, Substring.any, anyAux_of_valid]