proposition: Lemma all_clients_false_locks_correct_server_update : forall sigma st, (forall c, held (sigma (Client c)) = false) -> locks_correct (update name_eq_dec sigma Server st).
proof: Proof. Proof using. unfold locks_correct. intros. rewrite_update. now find_higher_order_rewrite. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)