fact: Definition is_inc_dec (m : Message) := match m with | inc_dec _ => true | _ => false end.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm