Why a scoped identity does not transfer to an insertion

A physical comparison also has to match products, domains, normalization, state-dependent data when relevant, and the observable itself. Lemma lem:transport is an elementary conditional interface, not a supplied map from $S_{\mathrm{inv}}$ to a clock insertion.