proposition: Lemma init_parent_cr : forall s1 s2 : Site, parent config_init s1 s2 -> dt config_init s1 < dt config_init s2.
proof: Proof. intros; absurd (parent config_init s1 s2). apply init_no_parent. trivial. Qed.
imports: DistributedReferenceCounting.machine0.machine counting