no goals
α : Type u_1
β : Type u_2
l : List α
f : α → List β
⊢ (∀ (l_1 : List β), l_1 ∈ map f l → l_1 = []) ↔ ∀ (x : α), x ∈ l → f x = []
simp only [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]