Reduce to binary string outputs with the encoding of Lemma 5.6 and Lemma 5.5. Factorise the two terms as a common lift followed by drops (Lemmas 7.4 and 7.2). The two drops have the same denotation, so they are provably equivalent by Lemma 7.3 and Lemma 6.1, and the common lift is cancelled with Lemma 5.5.