proposition: Lemma no_inc_send_table : forall (t0 : Send_table) (s0 s1 : Site), s0 <> s1 -> Inc_send_table t0 s0 s1 = t0 s1.
proof: Proof. intros; unfold Inc_send_table in |- *; apply other_site; auto. Qed.
imports: DistributedReferenceCounting.machine0.machine