Theorem 7.7 (Provable simplification of rational terms). Consider rational terms $f, g : A \to N^*$, where $N$ is a finite alphabet. There is a type $B$ and a surjective rational term $\pi : B \to A$, such that $\pi \mathbin{;} f$ and $\pi \mathbin{;} g$ are equivalent to simple rational terms.

This is a strengthening of Theorem 2.9 in which the decomposition is carried out within the equational system: surjectivity of $\pi$ is the provable notion of Definition 5.4, and the equivalences are provable.