Compatibility import for the quotient-level local-to-cumulative identity. The proof now lives with the decomposition machinery that uses it.