English
If l1, l2 are permutation-equivalent and l1 has nodupkeys, then kunion with any fixed list on the left preserves permutation.
Русский
Если l1 и l2 перестановочно эквиваленты и у l1 узлы повторов отсутствуют, то добавление слева фиксированного списка сохраняет перестановку.
LaTeX
$$$\\forall l,\\forall l_1,l_2:\\text{List}(\\Sigma \\beta),\\; l_1.\\NodupKeys \\to l_1 \\sim l_2 \\to kunion\\ l\\ l_1 \\sim kunion\\ l\\ l_2$$$
Lean4
theorem kunion_left : ∀ (l) {l₁ l₂ : List (Sigma β)}, l₁.NodupKeys → l₁ ~ l₂ → kunion l l₁ ~ kunion l l₂
| [], _, _, _, p => p
| s :: l, _, _, nd₁, p => ((p.kerase nd₁).kunion_left l <| nd₁.kerase s.1).cons s
