intro h
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
i : Nat
⊢ queue[i]? = none → queue.events[i]? = none
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
i : Nat
h : queue[i]? = none
⊢ queue.events[i]? = none