proposition: Lemma InputHandler_lbcases : forall h i st l out st' ms, InputHandler h i st = (l, out, st', ms) -> (exists c, h = Client c /\ ((i = Lock /\ out = [] /\ st' = st /\ ms = [(Server, Lock)] /\ l = InputLock c) \/ (l = InputUnlock c /\ i = Unlock /\ out = [] /\ held st' = false /\ ((held st = true /\ ms = [(Server, Unlock)]) \/ (st' = st /\ ms = []))))) \/ (out = [] /\ st' = st /\ ms = [] /\ l = Nop).
proof: Proof. Proof using. handler_unfold. intros. repeat break_match; repeat tuple_inversion; subst; simpl in *; subst; simpl in *. - left. eexists. intuition. - left. eexists. intuition. - left. eexists. intuition. - auto. - auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)