proposition: Lemma sigma_f_null : forall (E : Set) (f : E -> Z) (l : list E), (forall x_ : E, f x_ = 0%Z) -> sigma E l f = 0%Z.
proof: Proof. intros; elim l; simpl in |- *. omega. intros; generalize (H a); omega. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8