proposition: Lemma that_queue : forall (E : Set) (f : Site -> Site -> E) (s0 s1 : Site) (x : E), change_queue E f s0 s1 x s0 s1 = x.
proof: Proof. intros; unfold change_queue in |- *; unfold update2_table in |- *; apply here2. Qed.
imports: List fifo table reduce sigma2