simp [nextTime]
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ Option.isSome queue.events[0]? = true
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome
        (match queue[0]? with
        | none => none
        | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
      true ↔
    Option.isSome queue.events[0]? = true