Theorem: Queue.getElem?_some_events_getElem?_some (Runtime/Utilities/Queue.lean)

State before:
ε : 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
Tactic:
intro h
State after:
ε : 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

State before:
ε : 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
Tactic:
sorry
State after:
no goals