permutations'Aux_eq_permutationsAux2

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]

Похожие утверждения