Theorem: List.map_disj (Logic/Logic/LogicSymbol.lean)

State before:
α : Type u_1
inst✝² : LogicalConnective α
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
l : List α
⊢ f l.disj ↔ ∃ a ∈ l, f a
Tactic:
induction l <;> simp[*]
State after:
no goals