English
A fold over L using permutationsAux2 equals concatenating flats of each y's permutations with r.
Русский
Свёртка по L с использованием permutationsAux2 эквивалентна конкатенации плоских списков из каждой перестановки y и r.
LaTeX
$$$\forall {\alpha}, {t}:{\alpha}, {ts}:{List\;\alpha}, {r:L}, {L}:{List\{List\alpha\}},\;\; \mathrm{foldr} (\\lambda y r. (permutationsAux2 t ts r y id).2) r L = (L.flatMap (\\lambda y. (permutationsAux2 t ts [] y id).2)) ++ r$$$
Lean4
theorem foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) :
foldr (fun y r => (permutationsAux2 t ts r y id).2) r L =
(L.flatMap fun y => (permutationsAux2 t ts [] y id).2) ++ r :=
by
induction L with
| nil => rfl
| cons l L ih => simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]
