proposition: Lemma cardinal_collect_message : forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), first Message (b s1 s2) = value Message m -> cardinal (Collect_message Message b s1 s2 s1 s2) = (cardinal (b s1 s2) - cardinal_count m)%Z.
proof: Proof. intros. unfold cardinal in |- *. apply reduce_collect_message. auto. Qed.
imports: reduce DistributedReferenceCounting.machine2.cardinal sigma2 sum