English
Applying map twice to the left components and then permutations preserves the snd component of permutationsAux2.
Русский
Дважды применения map к левым компонентам через permutations сохранит snd компоненты permutationsAux2.
LaTeX
$$$\forall {\alpha}, {\beta}, {\alpha'}, {\beta'} (g:\alpha \to \alpha') (t:\alpha) (ts ys : List\alpha) :\;\mathrm{map}\; (\mathrm{map}\; g)\; (List.permutationsAux2\ t\ ts\ []\ ys\ id).2 = (List.permutationsAux2 (g t) (List.map g ts) [] (List.map g ys) id).2$$$
Lean4
theorem map_map_permutationsAux2 {α'} (g : α → α') (t : α) (ts ys : List α) :
map (map g) (permutationsAux2 t ts [] ys id).2 = (permutationsAux2 (g t) (map g ts) [] (map g ys) id).2 :=
map_permutationsAux2' _ _ _ _ _ _ _ _ fun _ => rfl
