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

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

case cons
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ :
  ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
⊢ b ∈ dlookup a (kunion (head✝ :: tail✝) l₂) ↔
    b ∈ dlookup a (head✝ :: tail✝) ∨ ¬a ∈ keys (head✝ :: tail✝) ∧ b ∈ dlookup a l₂
case nil => simp
no goals
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
l₂ : List (Sigma β)
⊢ b ∈ dlookup a (kunion [] l₂) ↔ b ∈ dlookup a [] ∨ ¬a ∈ keys [] ∧ b ∈ dlookup a l₂
simp
case mk
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
s : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
⊢ b ∈ dlookup a (kunion (s :: tail✝) l₂) ↔ b ∈ dlookup a (s :: tail✝) ∨ ¬a ∈ keys (s :: tail✝) ∧ b ∈ dlookup a l₂
cases' s with a'
case pos
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : a = a'
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂

case neg
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
case mk
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
by_cases h₁ : a = a'
case pos
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
snd✝ : β a
⊢ b ∈ dlookup a (kunion ({ fst := a, snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a, snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a, snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
case pos
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : a = a'
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
subst h₁
no goals
case pos
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
snd✝ : β a
⊢ b ∈ dlookup a (kunion ({ fst := a, snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a, snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a, snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
simp
case neg
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ : b ∈ dlookup a (kunion tail✝ (kerase a' l₂)) ↔
  b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a (kerase a' l₂) :=
  ih
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
case neg
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
let h₂ := @ih (kerase a' l₂)
case neg
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ :
  dlookup a (kunion tail✝ (kerase a' l₂)) = some b ↔ dlookup a tail✝ = some b ∨ ¬a ∈ keys tail✝ ∧ dlookup a l₂ = some b
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
case neg
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ : b ∈ dlookup a (kunion tail✝ (kerase a' l₂)) ↔
  b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a (kerase a' l₂) :=
  ih
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
simp [h₁] at h₂
no goals
case neg
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
b : β a
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, b ∈ dlookup a (kunion tail✝ l₂) ↔ b ∈ dlookup a tail✝ ∨ ¬a ∈ keys tail✝ ∧ b ∈ dlookup a l₂
l₂ : List (Sigma β)
a' : α
snd✝ : β a'
h₁ : ¬a = a'
h₂ :
  dlookup a (kunion tail✝ (kerase a' l₂)) = some b ↔ dlookup a tail✝ = some b ∨ ¬a ∈ keys tail✝ ∧ dlookup a l₂ = some b
⊢ b ∈ dlookup a (kunion ({ fst := a', snd := snd✝ } :: tail✝) l₂) ↔
    b ∈ dlookup a ({ fst := a', snd := snd✝ } :: tail✝) ∨
      ¬a ∈ keys ({ fst := a', snd := snd✝ } :: tail✝) ∧ b ∈ dlookup a l₂
simp [h₁, h₂]