proposition: Lemma clients_get_lock_messages : forall n c s, event_step_star step_async step_async_init (hd s) -> lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> Nth (queue (nwState (evt_a (hd s)) Server)) (S n) c -> eventually (fun s => In (mkPacket Server (Client c) Locked) (nwPackets (evt_a (hd s)))) s.
proof: Proof. Proof using. intros. pose proof (@clients_move_way_up_in_queue n 0 c s). pose proof (Nat.le_0_l n). repeat concludes. conclude_using (intuition; congruence). eapply eventually_monotonic_simple; [|eauto]. intros. simpl in *. intuition. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)