Soundness is checked axiom by axiom against the denotational semantics. For completeness, let $f, g : A → B$ have the same denotation. Postcomposing with the injective binary encoding $enc : B → 2*$ of Lemma 5.6, Theorem 7.7 (provable simplification) gives a surjective term $π$ such that $π ; f ; enc$ and $π ; g ; enc$ are provably equivalent to simple rational terms. These have the same denotation, so they are provably equivalent by Lemma 6.1, and $π$ and $enc$ are cancelled with Lemma 5.5.