constructor
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ { x | x ∈ l₁ ∨ x = head✝ ∨ x ∈ tail✝ } = { x | x ∈ l₁ } ∪ { x | x = head✝ ∨ x ∈ tail✝ }
no goals