no goals
α : Type u
β : Type v
γ : Type w
f : α → β
⊢ sublists' (map f []) = map (map f) (sublists' [])
simp
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
a : α
l : List α
⊢ sublists' (map f (a :: l)) = map (map f) (sublists' (a :: l))
simp [map_cons, sublists'_cons, sublists'_map f l, Function.comp]