Theorem: Queue.getElem?_none_events_getElem?_none (Runtime/Utilities/Queue.lean)

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

State before:
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
i : Nat
h : queue[i]? = none
⊢ queue.events[i]? = none
Tactic:
sorry
State after:
no goals