Round-six lemma `copy_facts`