Typebase should automatically generate simp rules for `a <> f a` where f is a recursive constructor.

[ordinarymath]

One such example that is currently manually proved is xs <> x :: xs