pub broadcast proof fn always_and_equality<T>(p: TempPred<T>, q: TempPred<T>)Expand description
ensures
#[trigger] always(p.and(q)) == always(p).and(always(q)),StatePred::and distributes over □.
§Postconditions
□(p ∧ q) == □p ∧ □q