case nil
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : ¬a ∈ keys []
⊢ dlookup a (kunion [] l₂) = dlookup a l₂

case cons
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : ∀ {l₂ : List (Sigma β)}, ¬a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a l₂
l₂ : List (Sigma β)
h : ¬a ∈ keys (head✝ :: tail✝)
⊢ dlookup a (kunion (head✝ :: tail✝) l₂) = dlookup a l₂
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : ¬a ∈ keys l₁
⊢ dlookup a (kunion l₁ l₂) = dlookup a l₂
induction l₁ generalizing l₂
case cons
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ : ∀ {l₂ : List (Sigma β)}, ¬a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a l₂
l₂ : List (Sigma β)
h : ¬a ∈ keys (head✝ :: tail✝)
⊢ dlookup a (kunion (head✝ :: tail✝) l₂) = dlookup a l₂
case nil
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : ¬a ∈ keys []
⊢ dlookup a (kunion [] l₂) = dlookup a l₂

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