proposition: Lemma true_set_rec_table : forall (r0 : Rec_table) (s0 : Site), Set_rec_table r0 s0 s0 = true.
proof: Proof. intros; unfold Set_rec_table in |- *; apply that_site. Qed.
imports: DistributedReferenceCounting.machine0.machine