α : Type u_1
a : α
l : List α
⊢ List.map (ofList ∘ List.cons a) (sublists' l) = List.map (cons a ∘ ofList) (sublists' l)
α : Type u_1
a : α
l : List α
⊢ powersetAux' (a :: l) = powersetAux' l ++ List.map (cons a) (powersetAux' l)
simp [powersetAux']
no goals
α : Type u_1
a : α
l : List α
⊢ List.map (ofList ∘ List.cons a) (sublists' l) = List.map (cons a ∘ ofList) (sublists' l)
rfl