proposition: Lemma same_parent : forall (c : Config) (s2 s5 s6 : Site), parent c s5 s6 -> parent c s2 s6 -> s2 = s5.
proof: Proof. intros. generalize H0. elim H. intros. generalize H2. elim H3. intros. generalize H5 H6. elim (bm c s4 owner). simpl in |- *. intuition. intro. simpl in |- *. case d. auto. intro. case (eq_site_dec s s3); intro. case (eq_site_dec s s1); intro. rewrite <- e; rewrite e0. auto. intuition. intuition. auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4