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