Proof of cancellation of permutations

Proposition (Cancellation of permutations). For any term f such that [[f]] = [[p ; g]] we can find f such that f = p ; f and [[f]] = [[g]].

Proof. Define p* to be the permutation:

id* = id
(p ; q)* = q* ; p*
(p q)* = p* q*
symm* = symm

Show by induction on p that p ; p* = id, and p* ; p = id. If we let f be p* ; f, then it is routine to check that it satisfies our requirements.