pub broadcast proof fn state_pred_and_apply_equality<T>(p: StatePred<T>, q: StatePred<T>, s: T)Expand description
ensures
#[trigger] p.and(q).apply(s) == (p.apply(s) && q.apply(s)),Lift StatePred::and to Verus meta-level.