Theorem: not_mem_cons_of_ne_of_not_mem (Talk/10Aesop.lean)

State before:
α : Type u_1
a y : α
l : List α
⊢ a ≠ y → ¬a ∈ l → ¬a ∈ y :: l
Tactic:
aesop
State after:
no goals