α : Type u_1
a : α
s : Multiset α
l : List α
⊢ List.map ofList (sublists' l) ++ List.map (ofList ∘ List.cons a) (sublists' l) ~
    List.map ofList (sublists' l) ++ List.map ((fun x => a ::ₘ x) ∘ ofList) (sublists' l)
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ powerset (a ::ₘ Quotient.mk (isSetoid α) l) =
    powerset (Quotient.mk (isSetoid α) l) + map (cons a) (powerset (Quotient.mk (isSetoid α) l))
simp
no goals
α : Type u_1
a : α
s : Multiset α
l : List α
⊢ List.map ofList (sublists' l) ++ List.map (ofList ∘ List.cons a) (sublists' l) ~
    List.map ofList (sublists' l) ++ List.map ((fun x => a ::ₘ x) ∘ ofList) (sublists' l)
rfl