proposition: Lemma ancestor_not_reflexive : forall c : Config, legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> s1 <> s2.
proof: Proof. intros. apply mul_ancestor_not_reflexive with (c := c). auto. apply ancestor_is_mul_ancestor. auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4