pub broadcast proof fn lift_state_not_equality<T>(p: StatePred<T>)Expand description
ensures
lift_state(p.not()) == not(lift_state(p)),StatePred::not distributes over lift_state.
ยงPostconditions
lift_state(!p) == !lift_state(p)