have in_set := listInSet l y h
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
⊢ y ∈ span { x | x ∈ l }
α : Type u_1
inst✝ : Semiring α
l : List α
y : α
h : y ∈ l
in_set : y ∈ asSet l
⊢ y ∈ span { x | x ∈ l }