proposition: Lemma InputUnlock_enabled : forall s c, lb_step_execution lb_step_async s -> now (enabled lb_step_async (InputUnlock c)) s.
proof: Proof. Proof using. intros. destruct s. simpl. unfold enabled, enabled. pose proof (InputHandler_Client_Unlock c (nwState (evt_a e) (Client c))). break_exists. repeat eexists. unfold InputHandler in *. unfold ClientIOHandler in *. eapply LabeledStepAsync_input with (h := (Client c)) (inp := Unlock); eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)