Round-six lemma `hdr_in`