Use cbn instead of simpl in [simpl rewrite]

[cbn] is better-behaved, and this will be necessary for some automation
in functoriality of adjoints.
wip