proof011.idr:19:9:When checking right hand side of vassoc' with expected type
        (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
                                                                 xs ++
                                                                 ys ++ zs =
                                                                 x ::
                                                                 (xs ++ ys) ++
                                                                 zs
proof011a.idr:13:9:When checking right hand side of vassoc' with expected type
        (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

rewriting xs ++ ys ++ xs to (xs ++ ys) ++ xs did not change type x ::
                                                                 xs ++
                                                                 ys ++ zs =
                                                                 x ::
                                                                 (xs ++ ys) ++
                                                                 zs