simp [asSet]
case nil
α : Type u_1
l₁ : List α
⊢ asSet (l₁ ++ []) = asSet l₁ ∪ asSet []

case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)
case cons
α : Type u_1
l₁ : List α
head✝ : α
tail✝ : List α
tail_ih✝ : asSet (l₁ ++ tail✝) = asSet l₁ ∪ asSet tail✝
⊢ asSet (l₁ ++ head✝ :: tail✝) = asSet l₁ ∪ asSet (head✝ :: tail✝)