case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
nd : NodupKeys []
⊢ ¬a ∈ keys (kerase a [])

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : NodupKeys tail✝ → ¬a ∈ keys (kerase a tail✝)
nd : NodupKeys (head✝ :: tail✝)
⊢ ¬a ∈ keys (kerase a (head✝ :: tail✝))
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
nd : NodupKeys l
⊢ ¬a ∈ keys (kerase a l)
induction l
case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : NodupKeys tail✝ → ¬a ∈ keys (kerase a tail✝)
nd : NodupKeys (head✝ :: tail✝)
⊢ ¬a ∈ keys (kerase a (head✝ :: tail✝))
case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
nd : NodupKeys []
⊢ ¬a ∈ keys (kerase a [])

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : NodupKeys tail✝ → ¬a ∈ keys (kerase a tail✝)
nd : NodupKeys (head✝ :: tail✝)
⊢ ¬a ∈ keys (kerase a (head✝ :: tail✝))
case nil => simp
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
nd : NodupKeys []
⊢ ¬a ∈ keys (kerase a [])
simp
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
⊢ ¬a ∈ keys (kerase a (hd :: tl))
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : NodupKeys (hd :: tl)
⊢ ¬a ∈ keys (kerase a (hd :: tl))
simp at nd
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
h : a = hd.fst
⊢ ¬a ∈ keys (kerase a (hd :: tl))

case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
h : ¬a = hd.fst
⊢ ¬a ∈ keys (kerase a (hd :: tl))
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
⊢ ¬a ∈ keys (kerase a (hd :: tl))
by_cases h : a = hd.1
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
ih : NodupKeys tl → ¬hd.fst ∈ keys (kerase hd.fst tl)
⊢ ¬hd.fst ∈ keys (kerase hd.fst (hd :: tl))
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
h : a = hd.fst
⊢ ¬a ∈ keys (kerase a (hd :: tl))
subst h
no goals
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
ih : NodupKeys tl → ¬hd.fst ∈ keys (kerase hd.fst tl)
⊢ ¬hd.fst ∈ keys (kerase hd.fst (hd :: tl))
simp [nd.1]
no goals
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : NodupKeys tl → ¬a ∈ keys (kerase a tl)
nd : ¬hd.fst ∈ keys tl ∧ NodupKeys tl
h : ¬a = hd.fst
⊢ ¬a ∈ keys (kerase a (hd :: tl))
simp [h, ih nd.2]