Round-six lemma `axP2_sp`