case nil
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion [] l₂) ↔ a ∈ keys [] ∨ a ∈ keys 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 (kunion tail✝ l₂) ↔ a ∈ keys tail✝ ∨ a ∈ keys l₂
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion (head✝ :: tail✝) l₂) ↔ a ∈ keys (head✝ :: tail✝) ∨ a ∈ keys l₂
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
⊢ a ∈ keys (kunion l₁ l₂) ↔ a ∈ keys l₁ ∨ a ∈ keys 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 (kunion tail✝ l₂) ↔ a ∈ keys tail✝ ∨ a ∈ keys l₂
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion (head✝ :: tail✝) l₂) ↔ a ∈ keys (head✝ :: tail✝) ∨ a ∈ keys l₂
case nil
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion [] l₂) ↔ a ∈ keys [] ∨ a ∈ keys 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 (kunion tail✝ l₂) ↔ a ∈ keys tail✝ ∨ a ∈ keys l₂
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion (head✝ :: tail✝) l₂) ↔ a ∈ keys (head✝ :: tail✝) ∨ a ∈ keys 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 (kunion tail✝ l₂) ↔ a ∈ keys tail✝ ∨ a ∈ keys l₂
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion (head✝ :: tail✝) l₂) ↔ a ∈ keys (head✝ :: tail✝) ∨ a ∈ keys l₂
case cons s l₁ ih => by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]
no goals
α : Type u
β : α → Type v
l l₁ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion [] l₂) ↔ a ∈ keys [] ∨ a ∈ keys l₂
simp
no goals
α : Type u
β : α → Type v
l l₁✝ l₂✝ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
l₁ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∈ keys (kunion l₁ l₂) ↔ a ∈ keys l₁ ∨ a ∈ keys l₂
l₂ : List (Sigma β)
⊢ a ∈ keys (kunion (s :: l₁) l₂) ↔ a ∈ keys (s :: l₁) ∨ a ∈ keys l₂
by_cases h : a = s.1 <;> [simp [h]; simp [h, ih]]