proposition: Lemma post_here : forall (b0 : Bag_of_message) (m0 : Message) (s0 s1 : Site), Post_message m0 b0 s0 s1 s0 s1 = input Message m0 (b0 s0 s1).
proof: Proof. intros; unfold Post_message in |- *; apply that_queue. Qed.
imports: counting