proposition: Lemma locks_correct_input_handlers : forall h i sigma u st' out ms, InputHandler h i (sigma h) = (u, out, st', ms) -> locks_correct sigma -> locks_correct (update name_eq_dec sigma h st').
proof: Proof. Proof using. set_up_input_handlers; auto using locks_correct_update_false. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)