English
Erasing first a then a' yields the same result as erasing a' then a: kerase a' (kerase a l) = kerase a (kerase a' l). When a = a' the two sides are identical; otherwise, the order does not matter.
Русский
Удаление сначала a, затем a' даёт такой же результат, как и удаление сначала a', затем a: kerase a' (kerase a l) = kerase a (kerase a' l).
LaTeX
$$$\forall {a a'} {l : List (\Sigma \beta)}, kerase\ a'\ (kerase\ a\ l) = kerase\ a\ (kerase\ a'\ l)$$$
Lean4
theorem kerase_kerase {a a'} {l : List (Sigma β)} : (kerase a' l).kerase a = (kerase a l).kerase a' :=
by
by_cases h : a = a'
· subst a'; rfl
induction l with
| nil => rfl
| cons x xs =>
by_cases a' = x.1
· subst a'
simp [kerase_cons_ne h, kerase_cons_eq rfl]
by_cases h' : a = x.1
· subst a
simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
· simp [kerase_cons_ne, *]
