proposition: Lemma other_queue : forall (E : Set) (f : Site -> Site -> E) (s0 s1 s2 s3 : Site) (x : E), s2 <> s0 \/ s3 <> s1 -> change_queue E f s0 s1 x s2 s3 = f s2 s3.
proof: Proof. intros; unfold change_queue in |- *; unfold update2_table in |- *; apply elsewhere2; trivial. Qed.
imports: List fifo table reduce sigma2