no goals
ι : Type ?u.369210
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
x : α
⊢ reduceOption (concat l (some x)) = concat (reduceOption l) x
simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some]