fact: Definition new_sigma2_but_table (t : Table2) := sigma2_table Site LS1 LS2 Data (fun (s2 s3 : Site) (d : Data) => if eq_site_dec s2 s0 then if eq_site_dec s3 s1 then 0%Z else f s2 s3 d else f s2 s3 d) t.
imports: List fifo table reduce