rw [Queue.isEmpty, ←Array.getElem?_zero_isSome_iff_not_isEmpty]
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ ¬isEmpty queue = true
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome (nextTime queue) = true ↔ Option.isSome queue.events[0]? = true