proposition: Lemma ancestor_rt2 : forall c : Config, legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> rt c s2 = true.
proof: Proof. intros. elim H0. intros. elim H1. auto. intros. elim H3; auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4