Round-six lemma `zextP_spec`