proposition: Lemma locks_correct_locked_input_handlers_old : forall h i sigma u st' out ms p, InputHandler h i (sigma h) = (u, out, st', ms) -> locks_correct sigma -> locks_correct_locked sigma p -> locks_correct_locked (update name_eq_dec sigma h st') p.
proof: Proof. Proof using. set_up_input_handlers. destruct (pBody p) eqn:?. - auto using locks_correct_locked_sent_lock. - auto using locks_correct_locked_sent_unlock. - now erewrite locked_in_flight_all_clients_false in * by eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)