Round-six lemma `bwd_body`