intro h
ε : Type
inst✝ : EventType ε
bound : Time
event : { e // bound ≤ time e }
queue : Queue ε bound
i : Nat
⊢ queue[i]? = some event → queue.events[i]? = some event.val
ε : Type
inst✝ : EventType ε
bound : Time
event : { e // bound ≤ time e }
queue : Queue ε bound
i : Nat
h : queue[i]? = some event
⊢ queue.events[i]? = some event.val