The completeness rule and the conjugacy rule are proved together by induction on the nesting depth of lists in the input type. The completeness rule follows the proof of Theorem 2.6. For the conjugacy rule with a nonempty value $w$ of length $k$, Lemmas 6.4 and 6.5 reduce to co-pairings of $k$-guarded nonempty terms. After grouping the list into bundles of size at least $k$ with the bundle lemma (Lemma 6.7), the bundled terms become syntactically $w$-conjugate, by the induction hypothesis, and Lemma 6.2 applies. The bundle isomorphism is cancelled with Lemma 5.5.