Theorem: Queue.all_events_bounded (Runtime/Utilities/Queue.lean)

State before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ ∀ {event : ε}, event ∈ queue.events.data → bound ≤ time event
Tactic:
sorry
State after:
no goals