English
Let α be a type and xs, ys be lists over α. If xs is contained in ys (xs ⊆ ys), then xs ∪ ys = ys.
Русский
Пусть α — тип, xs и ys — списки по α. Если xs ⊆ ys, то xs ∪ ys = ys.
LaTeX
$$$\\\\forall {\\\\alpha} [\\\\mathrm{DecidableEq} \\\\alpha] {xs, ys : \\\\mathrm List \\\\alpha},\n xs \\\\subseteq ys \\\rightarrow xs \\\\cup ys = ys$$$
Lean4
theorem union_eq_right {xs ys : List α} (h : xs ⊆ ys) : xs ∪ ys = ys := by
induction xs with
| nil => simp
| cons x xs ih =>
rw [cons_union, insert_of_mem <| mem_union_right _ <| h mem_cons_self, ih <| subset_of_cons_subset h]