proposition: Lemma sigma_same_table2 : forall t1 t2 : Site -> Z, sigma_table Site LS Z Z_id (fun_minus Site t1 t2) = (sigma_table Site LS Z Z_id t1 - sigma_table Site LS Z Z_id t2)%Z.
proof: Proof. intros t1 t2. unfold sigma_table in |- *. elim LS. simpl in |- *. auto. intros a l H. simpl in |- *. rewrite H. unfold fun_minus in |- *. rewrite Z_id_reduce. rewrite Z_id_reduce. rewrite Z_id_reduce. omega. Qed.
imports: List fifo table reduce