proof011.idr:20:5-21:18:
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:14:5-37:
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