proposition: Lemma sigma_but_null : forall (f : Site -> Z) (l : list Site), (forall s : Site, s <> owner -> f s = 0%Z) -> sigma_but Site owner eq_site_dec l f = 0%Z.
proof: Proof. simple induction l. simpl in |- *. auto. intros a l0 H H0. simpl in |- *. case (eq_site_dec a owner). intro e. apply H. exact H0. intros n. rewrite H0. rewrite H. auto. exact H0. auto. Qed.
imports: List fifo table reduce