English
For any a and list l, the sublists of a :: l are permuted as the concatenation of the sublists of l with the list obtained by preprending a to every sublist of l.
Русский
Для любого элемента a и списка l подсписки a :: l эквивалентны перестановке конкатенации подсписков l и списка, полученного добавлением a перед каждым подсписком l.
LaTeX
$$$$ \\mathrm{sublists}(\\mathrm{cons}\\; a\\; l) \\sim \\mathrm{sublists}\\; l \\;\\mathrm{append}\\; \\mathrm{map}(\\mathrm{cons}\\ a)\\; (\\mathrm{sublists}\\; l) $$$$
Lean4
theorem sublists_cons_perm_append (a : α) (l : List α) : sublists (a :: l) ~ sublists l ++ map (cons a) (sublists l) :=
Perm.trans (sublists_perm_sublists' _) <| by
rw [sublists'_cons]
exact Perm.append (sublists_perm_sublists' _).symm (Perm.map _ (sublists_perm_sublists' _).symm)
