pub open spec fn frame_preserving_update<P: PCM>(a: P, b: P) -> bool
{ forall |c| P::op(a, c).valid() ==> P::op(b, c).valid() }