case inr.inl he =>
  rw [isEmpty, Array.isEmpty_iff_data_eq_nil] at he
  simp [Membership.mem, he] at h
  contradiction
ε : Type
inst✝ : EventType ε
bound : Time
event : ε
queue₁ queue₂ : Queue ε bound
h : event ∈ queue₂
h✝ : ¬isEmpty queue₁ = true
he : isEmpty queue₂ = true
⊢ event ∈ queue₁
no goals