proposition: Lemma cardinal_post_message : forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), cardinal (Post_message Message m b s1 s2 s1 s2) = (cardinal (b s1 s2) + cardinal_count m)%Z.
proof: Proof. intros. unfold cardinal in |- *. apply reduce_post_message. Qed.
imports: reduce DistributedReferenceCounting.machine2.cardinal sigma2 sum