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