proposition: Lemma sigma_table_simpl2_property : forall (Data : Set) (t : Site -> Data) (P : (Site -> Data) -> Site -> Set) (f1 f2 : Site -> Data -> Z), (forall (s : Site) (d : Data), P t s -> f1 s d = f2 s d) -> (forall s : Site, P t s) -> sigma_table Site LS Data f1 t = sigma_table Site LS Data f2 t.
proof: Proof. intros Data0 t0 P f0 f3 H H0. unfold sigma_table in |- *. apply sigma_simpl. intros x H1. apply H. auto. Qed.
imports: List fifo table reduce