case nil
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h✝ : Nodup l₂✝
l₂ : List α
h : Nodup l₂
⊢ Nodup ([] ∪ l₂)

case cons
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
h✝ : Nodup l₂✝
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, Nodup l₂ → Nodup (l₁ ∪ l₂)
l₂ : List α
h : Nodup l₂
⊢ Nodup (a :: l₁ ∪ l₂)
α : Type u
β : Type v
l l₁✝ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
l₁ : List α
h : Nodup l₂
⊢ Nodup (l₁ ∪ l₂)
induction' l₁ with a l₁ ih generalizing l₂
no goals
case nil
α : Type u
β : Type v
l l₁ l₂✝ : List α
r : α → α → Prop
a b : α
inst✝ : DecidableEq α
h✝ : Nodup l₂✝
l₂ : List α
h : Nodup l₂
⊢ Nodup ([] ∪ l₂)
exact h
no goals
case cons
α : Type u
β : Type v
l l₁✝ l₂✝ : List α
r : α → α → Prop
a✝ b : α
inst✝ : DecidableEq α
h✝ : Nodup l₂✝
a : α
l₁ : List α
ih : ∀ {l₂ : List α}, Nodup l₂ → Nodup (l₁ ∪ l₂)
l₂ : List α
h : Nodup l₂
⊢ Nodup (a :: l₁ ∪ l₂)
exact (ih h).insert