α : Type u_1
l : List α
⊢ List.map ofList (sublists l) ~ powersetAux' l
α : Type u_1
l : List α
⊢ powersetAux l ~ powersetAux' l
rw [powersetAux_eq_map_coe]
no goals
α : Type u_1
l : List α
⊢ List.map ofList (sublists l) ~ powersetAux' l
exact (sublists_perm_sublists' _).map _