α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists' l ++ map (cons a) (sublists' l) ~ sublists l ++ map (cons a) (sublists l)
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists' (a :: l) ~ sublists l ++ map (cons a) (sublists l)
rw [sublists'_cons]
no goals
α : Type u
β : Type v
γ : Type w
a : α
l : List α
⊢ sublists' l ++ map (cons a) (sublists' l) ~ sublists l ++ map (cons a) (sublists l)
exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)