Round-six lemma `fwd_body`