proposition: Remark card_mess_diff : forall (q0 : queue Message) (m m' : Message), m <> m' -> card_mess m (input Message m' q0) = card_mess m q0.
proof: Proof. intros; unfold card_mess in |- *; apply input_diff_card; trivial. Qed.
imports: DistributedReferenceCounting.machine0.machine