English
Let l1 and l2 be lists with l1 a permutation of l2. Then for every n in N and every a in the element type, inserting a at position n in l1 yields a list permutation-equivalent to inserting a at position n in l2.
Русский
Пусть l1 и l2 — списки, и l1 является перестановкой l2. Тогда для любого n ∈ ℕ и любого a из типа элементов, списки, полученные вставкой a на позицию n в l1 и в l2, также переставимы (эквивалентны как перестановки).
LaTeX
$$$l_1 \\sim l_2 \\implies \\mathrm{insertIdx}(l_1,n,a) \\sim \\mathrm{insertIdx}(l_2,n,a)$$$
Lean4
@[gcongr]
protected theorem insertIdx {l₁ l₂ : List α} (h : l₁ ~ l₂) (n : ℕ) (a : α) : l₁.insertIdx n a ~ l₂.insertIdx n a :=
perm_insertIdx_iff.mpr h
