proposition: Lemma locks_correct_update_false : forall sigma st' x, locks_correct sigma -> held st' = false -> locks_correct (update name_eq_dec sigma (Client x) st').
proof: Proof. Proof using. unfold locks_correct. intuition. destruct (Name_eq_dec (Client x) (Client n)). - find_inversion. exfalso. rewrite_update. congruence. - rewrite_update. auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)