proposition: Lemma InputHandler_cases : forall h i st u out st' ms, InputHandler h i st = (u, out, st', ms) -> (exists c, h = Client c /\ ((i = Lock /\ out = [] /\ st' = st /\ ms = [(Server, Lock)]) \/ (i = Unlock /\ out = [] /\ held st' = false /\ ((held st = true /\ ms = [(Server, Unlock)]) \/ (st' = st /\ ms = []))))) \/ (out = [] /\ st' = st /\ ms = []).
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)