proposition: Lemma locks_correct_init : locks_correct init_handlers.
proof: Proof. Proof using. unfold locks_correct. simpl. discriminate. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)