simp only [not_mem_nil, not_false_eq_true, implies_true]
case nil
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.171629 → Type ?u.171631
α : Type u_1
β : Type ?u.171637
inst✝ : Monad m
⊢ [] = [] ↔ ∀ (a : α), a ∉ []
no goals