no goals
ι : Type ?u.348712
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
x : α
l : List (Option α)
⊢ reduceOption (some x :: l) = x :: reduceOption l
simp only [reduceOption, filterMap, id.def, eq_self_iff_true, and_self_iff]