proposition: Lemma locks_correct_locked_at_head_preserved : forall sigma st' p, locks_correct_locked sigma p -> (forall c, at_head_of_queue sigma c -> at_head_of_queue (update name_eq_dec sigma Server st') c) -> locks_correct_locked (update name_eq_dec sigma Server st') p.
proof: Proof. Proof using. unfold locks_correct_locked, valid_locked. intuition. break_exists. exists x. intuition. - firstorder. - now rewrite_update. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)