proposition: Lemma held_until_Unlock : forall c s, lb_step_execution lb_step_async s -> held (nwState (evt_a (hd s)) (Client c)) = true -> weak_until (fun s => held (nwState (evt_a (hd s)) (Client c)) = true) (next (fun s => In (mkPacket (Client c) Server Unlock) (nwPackets (evt_a (hd s))))) s.
proof: Proof. Proof using. intros c. cofix CIH. destruct s. simpl. intros. invcs H. invcs H3. - coinductive_case CIH. monad_unfold. unfold NetHandler in *. break_match_hyp. + find_apply_lem_hyp ClientNetHandler_cases. repeat find_rewrite. simpl. intuition; update_destruct_max_simplify; repeat find_rewrite; auto. + find_apply_lem_hyp ServerNetHandler_cases. repeat find_rewrite. simpl. intuition; break_exists; intuition; rewrite_update; repeat find_rewrite; auto. - monad_unfold. find_apply_lem_hyp InputHandler_lbcases. intuition; break_exists; intuition. + coinductive_case CIH. repeat find_rewrite. simpl. update_destruct_max_simplify; repeat find_rewrite; auto. + subst. destruct (fin_eq_dec _ c x). * clear CIH. subst. apply W0; simpl. fold LockServ_MultiParams in *. repeat find_rewrite. simpl. auto. * coinductive_case CIH. repeat find_rewrite. simpl. now rewrite_update. + coinductive_case CIH. clear CIH. repeat find_rewrite. simpl. update_destruct_max_simplify; repeat find_rewrite; auto. + coinductive_case CIH. clear CIH. repeat find_rewrite. simpl. update_destruct_max_simplify; repeat find_rewrite; auto. - coinductive_case CIH. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)