proposition: Lemma locks_correct_true_at_head_of_queue : forall sigma x, locks_correct sigma -> held (sigma (Client x)) = true -> at_head_of_queue sigma x.
proof: Proof. Proof using. unfold locks_correct. intros. find_apply_hyp_hyp. break_exists. eauto using at_head_of_queue_intro. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)