English
Folding the tail ts into the function argument commutes with taking the second projection of permutationsAux2 after appending ys.
Русский
Сворачивание хвоста ts внутрь аргумента функции вместе с оператором второй проекции permutationsAux2 после дописывания ys коммутируется.
LaTeX
$$$\forall {\alpha}, {\beta}, {t}:{\alpha}, {ts},{ys}: List\;\alpha, {r}: List\;\beta, (f : List\;\alpha \to \beta) : \\ ((permutationsAux2 t [] r ys) (\lambda x. f (x ++ ts))).2 = (permutationsAux2 t ts r ys f).2$$$
Lean4
/-- The `ts` argument to `permutationsAux2` can be folded into the `f` argument. -/
theorem permutationsAux2_comp_append {t : α} {ts ys : List α} {r : List β} (f : List α → β) :
((permutationsAux2 t [] r ys) fun x => f (x ++ ts)).2 = (permutationsAux2 t ts r ys f).2 := by
induction ys generalizing f with
| nil => simp
| cons ys_hd _ ys_ih => simp [ys_ih fun xs => f (ys_hd :: xs)]
