Do more coercion optimisation on the fly

When studying #15019 (closed), I looked at CoreOpt.pushCoValArg. I saw lots of attempted decompositions in pushCoValArg, which were trying to do decomposeFunCo on

    C @g1 ; sym (C @g2)
where
    axiom C a = a -> a

But the smart mkNthCo can't make progress on this, so we get

   Nth:2 (C @g1 ; sym (C @g2))

and these things stack up if there is a chain of applications in Simplify.simplCast.

The coercion optimiser will optimise this coercion to

   (g1 ; sym g2) -> (g1 ; sym g2)

and now the smart mkNthCo in decomposeFunCo will succeed.

Possible idea: make this optimization part of mkTransCo so that it happens on the fly.

(Annoyingly, I can't remember which of the three test cases mentioned in #15109 (closed) displayed this behaviour.)