proposition: Lemma InputHandler_Client_Unlock : forall c sigma, exists sigma' os ms, InputHandler (Client c) Unlock sigma = (InputUnlock c, os, sigma', ms).
proof: Proof. Proof using. intros. unfold InputHandler. unfold ClientIOHandler. monad_unfold. repeat break_let. find_inversion. eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)