English
The second component of permutationsAux2 when using a nil r respects an equality with a mapped form; more precisely, it matches the structure of the appended form under a consistency relation.
Русский
Вторая компонента permutationsAux2 при пустом r согласуется с отображенной формой; формулировка касается структуры добавления с сохранением консистентности.
LaTeX
$$$(permutationsAux2\ t\ ts\ nil\ ys\ id).2 = (permutationsAux2\ t\ nil\ nil\ ys\ id).2.map\text{...}$$$
Lean4
/-- The `r` argument to `permutationsAux2` is the same as appending. -/
theorem permutationsAux2_append (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) :
(permutationsAux2 t ts nil ys f).2 ++ r = (permutationsAux2 t ts r ys f).2 := by
induction ys generalizing f <;> simp [*]
