proposition: Lemma update_elsewhere : forall (d0 : Date_table) (s0 s1 : Site) (newdate : nat), s0 <> s1 -> Update_table d0 s0 newdate s1 = d0 s1.
proof: Proof. intros; unfold Update_table in |- *; apply other_site; trivial. Qed.
imports: DistributedReferenceCounting.machine0.machine