proposition: Lemma sigma_rooted_fun10 : forall s2 : Site, sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s owner s2 copy) = 0%Z.
proof: Proof. intros. apply sigma_but_null. intros. simpl in |- *. rewrite case_ineq. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2