intro h
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
⊢ event ∈ queue₂ → event ∈ merge queue₁ queue₂
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
⊢ event ∈ merge queue₁ queue₂