proposition: Lemma held_eventually_InputUnlock : forall c s, lb_step_execution lb_step_async s -> weak_fairness lb_step_async label_silent s -> eventually (now (occurred (InputUnlock c))) s.
proof: Proof. Proof using. intros. pose proof (@InputUnlock_continuously_enabled s c). intuition. eapply_prop_hyp weak_fairness cont_enabled; [|now unfold label_silent]. solve_by_inversion. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)