case cons
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a = s.fst ∨ a ∈ keys tail✝
⊢ dlookup a (kunion (s :: tail✝) l₂) = dlookup a (s :: tail✝)
α : 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₁ with s _ ih generalizing l₂ <;> simp at h
case cons.inl.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h : a = { fst := a', snd := snd✝ }.fst
⊢ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) = dlookup a ({ fst := a', snd := snd✝ } :: tail✝)

case cons.inr.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
⊢ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) = dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
case cons
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a = s.fst ∨ a ∈ keys tail✝
⊢ dlookup a (kunion (s :: tail✝) l₂) = dlookup a (s :: tail✝)
cases' h with h h <;> cases' s with a'
case cons.inl.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
snd✝ : β a
⊢ dlookup a (kunion ({ fst := a, snd := snd✝ } :: tail✝) l₂) = dlookup a ({ fst := a, snd := snd✝ } :: tail✝)
case cons.inl.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h : a = { fst := a', snd := snd✝ }.fst
⊢ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) = dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
subst h
no goals
case cons.inl.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
snd✝ : β a
⊢ dlookup a (kunion ({ fst := a, snd := snd✝ } :: tail✝) l₂) = dlookup a ({ fst := a, snd := snd✝ } :: tail✝)
simp
case cons.inr.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
⊢ dlookup a ({ fst := a', snd := snd✝ } :: kunion tail✝ (kerase { fst := a', snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
case cons.inr.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
⊢ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) = dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
rw [kunion_cons]
case pos
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
h' : a = a'
⊢ dlookup a ({ fst := a', snd := snd✝ } :: kunion tail✝ (kerase { fst := a', snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a', snd := snd✝ } :: tail✝)

case neg
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a ({ fst := a', snd := snd✝ } :: kunion tail✝ (kerase { fst := a', snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
case cons.inr.mk
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
⊢ dlookup a ({ fst := a', snd := snd✝ } :: kunion tail✝ (kerase { fst := a', snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
by_cases h' : a = a'
case pos
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
snd✝ : β a
⊢ dlookup a ({ fst := a, snd := snd✝ } :: kunion tail✝ (kerase { fst := a, snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a, snd := snd✝ } :: tail✝)
case pos
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
h' : a = a'
⊢ dlookup a ({ fst := a', snd := snd✝ } :: kunion tail✝ (kerase { fst := a', snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
subst h'
no goals
case pos
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
snd✝ : β a
⊢ dlookup a ({ fst := a, snd := snd✝ } :: kunion tail✝ (kerase { fst := a, snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a, snd := snd✝ } :: tail✝)
simp
no goals
case neg
α : Type u
β : α → Type v
l l₁✝ l₂✝¹ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂✝ : List (Sigma β)
h✝ : a ∈ keys l₁
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys tail✝ → dlookup a (kunion tail✝ l₂) = dlookup a tail✝
l₂ : List (Sigma β)
h : a ∈ keys tail✝
a' : α
snd✝ : β a'
h' : ¬a = a'
⊢ dlookup a ({ fst := a', snd := snd✝ } :: kunion tail✝ (kerase { fst := a', snd := snd✝ }.fst l₂)) =
    dlookup a ({ fst := a', snd := snd✝ } :: tail✝)
simp [h', ih h]