proposition: Lemma reduce_collect_message : forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), first Message (b s1 s2) = value Message m -> reduce Message f (Collect_message Message b s1 s2 s1 s2) = (reduce Message f (b s1 s2) - f m)%Z.
proof: Proof. intros m s1 s2 b H. rewrite collect_here. apply reduce_first_out. auto. Qed.
imports: List fifo table reduce sigma2