proposition: Lemma ancestor_is_mul_ancestor : forall (c : Config) (s1 s2 : Site), ancestor c s1 s2 -> mul_ancestor c s1 s2.
proof: Proof. intros. elim H. intros. apply mul_short. elim H0. intros. apply mul_parent_intro. auto. apply inc_dec_in. auto. auto. intros. apply mul_long with (s1 := s3). auto. elim H2. intros. apply mul_parent_intro. auto. apply inc_dec_in. auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4