Make simp right-normalises list append

[ordinarymath]

Currently list append is by default normalized left i.e. xs ++ (ys ++ zs) = (xs ++ ys) ++ zs This issue is about making it the opposite i.e. (xs ++ ys) ++ zs = xs ++ (ys ++ zs) Currently there is work in progress is in branch cons_append_norm

[mn200]

Actually, the branch is cons-append-norm (hyphens, not underscores).

[mn200]

As per work done in ad11e1b42fe716e, it's not so clear to me that we need to right-associate. Instead, we can just add one extra rewrite

(xs ++ (h::t)) ++ ys = xs ++ h::(t ++ ys)

and get a normalising, left-associated, confluent system.