English
The function permutationsAux2 builds a list of insertions of t into ts, producing a pair whose first component is ys ++ ts for any ys and f; the second component encodes the inserted permutations.
Русский
Функция permutationsAux2 строит список вставок t в ts, образуя пару, первую компоненту которой можно записать как ys ++ ts для любых ys и f; вторая компонента кодирует вставленные перестановки.
LaTeX
$$$(\forall t, ts, r, ys, f). (permutationsAux2\ t\ ts\ r\ ys\ f).1 = ys ++ ts$$$
Lean4
theorem permutationsAux2_fst (t : α) (ts : List α) (r : List β) :
∀ (ys : List α) (f : List α → β), (permutationsAux2 t ts r ys f).1 = ys ++ ts
| [], _ => rfl
| y :: ys, f => by simp [permutationsAux2, permutationsAux2_fst t _ _ ys]
