proposition: Lemma disjoint_case_for_site : forall s : Site, {s = owner} + {rt c0 s = false} + {direct_son s} + {indirect_son1 s}.
proof: Proof. intro. case (eq_site_dec s owner). intro. auto. intro. generalize (direct_or_indirect_son1 s). intro. elim (decide_rt s). intro. auto. intro. auto. elim H. auto. auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4