Theorem: ne_nil_of_mem (Talk/10Aesop.lean)

State before:
α : Type u_1
a : α
l : List α
h : a ∈ l
⊢ l ≠ []
Tactic:
aesop
State after:
no goals