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