proposition: Lemma locks_correct_locked_at_head : forall sigma p c, pDst p = Client c -> pBody p = Locked -> locks_correct_locked sigma p -> at_head_of_queue sigma c.
proof: Proof. Proof using. unfold locks_correct_locked. firstorder. repeat find_rewrite. find_inversion. eauto using at_head_of_queue_intro. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)