proposition: Lemma ancestor_transitive : forall s1 s2 s3 : Site, ancestor s1 s2 -> ancestor s2 s3 -> ancestor s1 s3.
proof: Proof. intros s1 s2 s3 H. intro. generalize H. elim H0. intros. apply long with (s1 := s0). auto. auto. intros. apply long with (s1 := s4). auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4