no goals
α : Type u_1
n : ℕ
a : α
s : Multiset α
l : List α
⊢ powersetLen (n + 1) (a ::ₘ Quotient.mk (isSetoid α) l) =
    powersetLen (n + 1) (Quotient.mk (isSetoid α) l) + map (cons a) (powersetLen n (Quotient.mk (isSetoid α) l))
simp [powersetLen_coe']