proposition: Lemma locks_correct_unlock_sent_lock : forall sigma p, pBody p = Lock -> locks_correct_unlock sigma p.
proof: Proof. Proof using. unfold locks_correct_unlock. intuition. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)