proposition: Lemma sigma_table_simpl : forall t1 t2 : Site -> Data, t1 = t2 -> sigma_table Site LS Data f t1 = sigma_table Site LS Data f t2.
proof: Proof. unfold sigma_table in |- *. intros t1 t2 H. apply sigma_simpl. intros x H0. rewrite H; auto. Qed.
imports: List fifo table reduce