[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?

Here's two implementations of break, a snappy one from the prelude, and a slow stupid stateful one. They are quickchecked to be identical. Is there a way to prove they are identical mathematically? What are the techniques involved? Or to transform one to the other? import Control.Monad.State import Test.QuickCheck tThis = take 5 . show . mybreak (>4000000) $ [1..10^7] tPrel = take 5 . show . prelbreak (>4000000) $ [1..10^7] prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) -- fast, more or less as implemented in prelude iiuc mybreak p xs = evalState (brk p) ([],xs) -- stateful, slow brk p = do (notsat,remaining) <- get case remaining of [] -> return (notsat,remaining) (r:rs) -> if p r then return (notsat,remaining) else do put (notsat++[r],rs) -- ++ is probaby a major reason brk p