rw [isEmpty, Array.isEmpty_iff_data_eq_nil] at he
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : isEmpty queue₂ = true
⊢ event ∈ queue₁
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : queue₂.events.data = []
⊢ event ∈ queue₁