proposition: Lemma locks_correct_unlock_at_head : forall sigma p c, pSrc p = Client c -> pBody p = Unlock -> locks_correct_unlock sigma p -> at_head_of_queue sigma c.
proof: Proof. Proof using. unfold locks_correct_unlock. intros. find_apply_hyp_hyp. clear H1. break_exists. unfold valid_unlock in *. intuition. break_exists. repeat find_rewrite. repeat find_inversion. eauto using at_head_of_queue_intro. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)