case nil
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
l₂ : List (Sigma β)
nd₁ : NodupKeys []
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion [] l₂)

case cons
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : ∀ {l₂ : List (Sigma β)}, NodupKeys tail✝ → NodupKeys l₂ → NodupKeys (List.kunion tail✝ l₂)
l₂ : List (Sigma β)
nd₁ : NodupKeys (head✝ :: tail✝)
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion (head✝ :: tail✝) l₂)
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
nd₁ : NodupKeys l₁
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion l₁ l₂)
induction l₁ generalizing l₂
case cons
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : ∀ {l₂ : List (Sigma β)}, NodupKeys tail✝ → NodupKeys l₂ → NodupKeys (List.kunion tail✝ l₂)
l₂ : List (Sigma β)
nd₁ : NodupKeys (head✝ :: tail✝)
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion (head✝ :: tail✝) l₂)
case nil
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
l₂ : List (Sigma β)
nd₁ : NodupKeys []
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion [] l₂)

case cons
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : ∀ {l₂ : List (Sigma β)}, NodupKeys tail✝ → NodupKeys l₂ → NodupKeys (List.kunion tail✝ l₂)
l₂ : List (Sigma β)
nd₁ : NodupKeys (head✝ :: tail✝)
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion (head✝ :: tail✝) l₂)
case nil => simp only [nil_kunion, nd₂]
no goals
case cons
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : ∀ {l₂ : List (Sigma β)}, NodupKeys tail✝ → NodupKeys l₂ → NodupKeys (List.kunion tail✝ l₂)
l₂ : List (Sigma β)
nd₁ : NodupKeys (head✝ :: tail✝)
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion (head✝ :: tail✝) l₂)
case cons s l₁ ih =>
  simp at nd₁
  simp [not_or, nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]
no goals
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
l₂ : List (Sigma β)
nd₁ : NodupKeys []
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion [] l₂)
simp only [nil_kunion, nd₂]
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, NodupKeys l₁ → NodupKeys l₂ → NodupKeys (List.kunion l₁ l₂)
l₂ : List (Sigma β)
nd₂ : NodupKeys l₂
nd₁ : ¬s.fst ∈ keys l₁ ∧ NodupKeys l₁
⊢ NodupKeys (List.kunion (s :: l₁) l₂)
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, NodupKeys l₁ → NodupKeys l₂ → NodupKeys (List.kunion l₁ l₂)
l₂ : List (Sigma β)
nd₁ : NodupKeys (s :: l₁)
nd₂ : NodupKeys l₂
⊢ NodupKeys (List.kunion (s :: l₁) l₂)
simp at nd₁
no goals
α : Type u
β : α → Type v
l : List (Sigma β)
inst✝ : DecidableEq α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, NodupKeys l₁ → NodupKeys l₂ → NodupKeys (List.kunion l₁ l₂)
l₂ : List (Sigma β)
nd₂ : NodupKeys l₂
nd₁ : ¬s.fst ∈ keys l₁ ∧ NodupKeys l₁
⊢ NodupKeys (List.kunion (s :: l₁) l₂)
simp [not_or, nd₁.1, nd₂, ih nd₁.2 (nd₂.kerase s.1)]