intro h
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
⊢ nextTime queue = some next → ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val
ε : Type
inst✝ : EventType ε
bound : Time
next : Time.From bound
queue : Queue ε bound
h : nextTime queue = some next
⊢ ∃ event, queue[0]? = some event ∧ time event.val ≥ next.val