α : Type u_1
n : ℕ
a : α
l : List α
⊢ List.map (ofList ∘ List.cons a) (sublistsLen n l) = List.map (cons a ∘ ofList) (sublistsLen n l)
α : Type u_1
n : ℕ
a : α
l : List α
⊢ powersetLenAux (n + 1) (a :: l) = powersetLenAux (n + 1) l ++ List.map (cons a) (powersetLenAux n l)
simp [powersetLenAux_eq_map_coe]
no goals
α : Type u_1
n : ℕ
a : α
l : List α
⊢ List.map (ofList ∘ List.cons a) (sublistsLen n l) = List.map (cons a ∘ ofList) (sublistsLen n l)
rfl