Remark: Relationship to the registered record condition

Diagonal faithfulness isolates the projective-diagonal property needed in the cocycle proof. A continuation record argument that has already identified Born future-test laws can imply this property by taking computational diagonals. The registered record equality itself, however, is an equality of classical observations of typed programs, not this residual equation. We therefore retain Definition def:df as an explicit conditional hypothesis.