English
Permutations with the Aux2 construction are equivalent to a standard permutations'Aux construction with a specific embedding.
Русский
Перестановки через конструкцию permutations'Aux эквивалентны стандартной permutations'Aux с конкретной вложенной записью.
LaTeX
$$$\forall {\alpha}, {\beta}, (t:\alpha) (ts:\ List\alpha):\; permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd$$$
Lean4
theorem permutations'Aux_eq_permutationsAux2 (t : α) (ts : List α) :
permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).2 :=
by
induction ts with
| nil => rfl
| cons a ts ih => ?_
simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq, cons.injEq, true_and]
simp +singlePass only [← permutationsAux2_append]
simp [map_permutationsAux2]