induction l with
| nil => simp only [not_mem_nil, not_false_eq_true, implies_true];
| cons a _ _ =>
  simp_all only [mem_cons, not_or, false_iff, not_forall, not_and, not_not];
  use a;
  tauto;
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
l : List α
⊢ l = [] ↔ ∀ (a : α), a ∉ l
no goals