Fix [rewrite∘A] by going through a constant

The tactics are written under the assumption that [cbv beta] is safe.
So we make it safe by replacing the notation by a new [Local Definition
compose].