Round-six lemma `orthB_sound`