The grouplift-drop factorisation of the appendix gives a group-lift $α : A → C$ with a one-sided inverse $α⁻¹$, i.e. $α ; α⁻¹ ≡ id$, such that $α⁻¹ ; f$ and $α⁻¹ ; g$ are provably equivalent to drops. By Lemma 7.3 there is a lift $σ : C → B$ with inverse $σ⁻¹$ such that $σ⁻¹$ composed with these drops gives simple rational terms. The term $π = σ⁻¹ ; α⁻¹$ is surjective, since $(α ; σ) ; π ≡ id$.