simp [merge]
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈ merge queue₁ queue₂
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈
    if isEmpty queue₁ = true then queue₂
    else
      if isEmpty queue₂ = true then queue₁
      else
        {
          events :=
            merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
              merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                (Array.split queue₂.events fun x => decide (time x = bound)).snd,
          sorted :=
            (_ :
              Sorted
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                      (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                    merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                      (Array.split queue₂.events fun x => decide (time x = bound)).snd).data),
          bounded :=
            (_ :
              ∀ {event : ε},
                (merge.mergeImmediate (Array.split queue₁.events fun x => decide (time x = bound)).fst
                          (Array.split queue₂.events fun x => decide (time x = bound)).fst ++
                        merge.mergeFuture (Array.split queue₁.events fun x => decide (time x = bound)).snd
                          (Array.split queue₂.events fun x => decide (time x = bound)).snd)[0]? =
                    some event →
                  bound ≤ time event) }