English
A variant stating the same mem condition using id as the identity function.
Русский
Вариант с тем же условием принадлежности, используя id в качестве тождественной функции.
LaTeX
$$$\forall {t},{ts},{ys},{l}: List\;\alpha, l \in (permutationsAux2 t ts [] ys id).2 \iff \exists l_1 l_2, l_2 \neq [] \land ys = l_1 ++ l_2 \land l = l_1 ++ t :: l_2 ++ ts$$$
Lean4
theorem mem_permutationsAux2' {t : α} {ts : List α} {ys : List α} {l : List α} :
l ∈ (permutationsAux2 t ts [] ys id).2 ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts := by
rw [show @id (List α) = ([] ++ ·) by funext _; rfl]; apply mem_permutationsAux2