proposition: Lemma InputLock_Lock : forall s c, lb_step_execution lb_step_async s -> now (occurred (InputLock c)) s -> next (fun s => In (mkPacket (Client c) Server Lock) (nwPackets (evt_a (hd s)))) s.
proof: Proof. Proof using. intros. invcs H. invcs H1. - monad_unfold. unfold NetHandler in *. break_match_hyp. + unfold occurred in *. find_apply_lem_hyp ClientNetHandler_lbcases; intuition; congruence. + unfold occurred in *. find_apply_lem_hyp ServerNetHandler_lbcases; intuition; break_exists; intuition; congruence. - monad_unfold. find_apply_lem_hyp InputHandler_lbcases. intuition; try congruence. break_exists. intuition; try congruence. fold LockServ_MultiParams in *. repeat find_rewrite. simpl. left. unfold occurred in *. congruence. - unfold occurred in *. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)