English
If two lists of Sigma β are permutations of each other, then their right kunion with any fixed list is also a permutation of each other.
Русский
Пусть два списка элементов вида Σβ являются перестановочно эквивалентны; тогда их правый kunion с любым фиксированным списком также переставим между собой.
LaTeX
$$$\\forall l_1,l_2:\\text{List}(\\Sigma \\beta),\\; l_1 \\sim l_2 \\rightarrow \\forall l:\\text{List}(\\Sigma \\beta),\\ kunion\\ l_1\\ l \\sim kunion\\ l_2\\ l$$$
Lean4
theorem kunion_right {l₁ l₂ : List (Sigma β)} (p : l₁ ~ l₂) (l) : kunion l₁ l ~ kunion l₂ l := by
induction p generalizing l with
| nil => rfl
| cons hd _ ih => simp [ih (List.kerase _ _)]
| swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
| trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)
