proposition: Lemma InputUnlock_continuously_enabled : forall s c, lb_step_execution lb_step_async s -> cont_enabled lb_step_async (InputUnlock c) s.
proof: Proof. Proof using. unfold cont_enabled. intros. apply always_continuously. eapply always_monotonic; [|eapply always_inv; eauto; eauto using lb_step_execution_invar]; eauto using InputUnlock_enabled. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition) Verdi(LabeledNet) InfSeqExt(infseq classical)