proposition: Lemma update_here : forall (d0 : Date_table) (s0 : Site) (newdate : nat), Update_table d0 s0 newdate s0 = newdate.
proof: Proof. intros; unfold Update_table in |- *; apply that_site. Qed.
imports: DistributedReferenceCounting.machine0.machine