constructor <;> split <;> simp_all [Option.isSome]
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
⊢ Option.isSome
        (match queue[0]? with
        | none => none
        | some nextEvent => some { val := time nextEvent.val, property := (_ : bound ≤ time nextEvent.val) }) =
      true ↔
    Option.isSome queue.events[0]? = true
case mp.h_2
ε : Type
inst✝ : EventType ε
bound : Time
queue : Queue ε bound
x✝ : Option { e // bound ≤ time e }
nextEvent✝ : { e // bound ≤ time e }
heq✝ : queue[0]? = some nextEvent✝
⊢ (match queue.events[0]? with
    | some val => true
    | none => false) =
    true