no goals
p : Char → Bool
s : String
⊢ revFind s p =
    Option.map (fun x => { byteIdx := utf8Len x }) (List.tail? (List.dropWhile (fun x => !p x) (List.reverse s.data)))
simpa using revFindAux_of_valid p s.1.reverse []