proposition: Lemma sigma_table_simpl_property : forall (t1 t2 : Site -> Data) (P : (Site -> Data) -> Site -> Set), ((forall d : Site, P t2 d) -> t1 = t2) -> (forall d : Site, P t2 d) -> sigma_table Site LS Data f t1 = sigma_table Site LS Data f t2.
proof: Proof. unfold sigma_table in |- *. intros t1 t2 P H H0. apply sigma_simpl. intros x H1. generalize (H H0). intro H2. rewrite H2. auto. Qed.
imports: List fifo table reduce