pub proof fn lemma_pcm_associative<P: PCM>()Expand description
ensures
forall |a: P, b: P, c: P| (#[trigger] P::op(a, P::op(b, c))) == P::op(P::op(a, b), c),Provides a quantified associativity fact about a partially commutative monoid.
Note that, to avoid trigger loops, it doesn’t provide associativity and thus
should not be used in the same context as lemma_pcm_properties