proposition: Lemma other_site : forall (E : Set) (f : Site -> E) (s0 s1 : Site) (x : E), s0 <> s1 -> change_site E f s0 x s1 = f s1.
proof: Proof. intros; unfold change_site in |- *; apply elsewhere; trivial. Qed.
imports: List fifo table