proposition: Remark add_reduce : forall x : Z, (x + 1 - 1)%Z = x.
proof: Proof. intro; omega. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4