English
Let t ∈ α and ts, is ∈ List α. Then the auxiliary permutations for t :: ts with is equals the fold over permutations of is, combined with permutationsAux2 t ts on each step.
Русский
Пусть t ∈ α и ts, is ∈ List α. Тогда перестановкиAux для t :: ts с is равны свёртке по permutations of is, объединённой с permutationsAux2 t ts на каждом шаге.
LaTeX
$$$$\mathrm{permutationsAux}(t :: ts)\; is = \mathrm{foldr}\left(\lambda y\, r,\; (\mathrm{permutationsAux2}\ t\ ts\ r\ y\ id).2\right)\left(\mathrm{permutationsAux}\ ts\ (t :: is)\right)\; (\mathrm{permutations}\; is).$$$$
Lean4
@[simp]
theorem permutationsAux_cons (t : α) (ts is : List α) :
permutationsAux (t :: ts) is =
foldr (fun y r => (permutationsAux2 t ts r y id).2) (permutationsAux ts (t :: is)) (permutations is) :=
by rw [permutationsAux, permutationsAux.rec]; rfl
