rw [← Mem.ToList.mem_iff_mem_toList]
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ toList empty
C : Type u
τ : outParam (Type v)
inst✝⁴ : Insert C τ
inst✝³ : Membership τ C
inst✝² : Mem C τ
inst✝¹ : ToList C τ
inst✝ : Mem.ToList C τ
x : τ
⊢ x ∉ empty