This is factored out of !558 (merged); so far we were unable to agree on good names for these two lemmas.