proposition: Lemma sigma_disjoint2 : sigma_table Site LS Data (fun_minus_site f1 f2) t = (sigma_table Site LS Data f1 t - sigma_table Site LS Data f2 t)%Z.
proof: Proof. unfold sigma_table, fun_minus_site in |- *. elim LS. simpl in |- *. trivial. intros a l H. simpl in |- *. rewrite H. omega. Qed.
imports: List fifo table reduce