case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
h : a ∈ keys []
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ [] = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a [] = l₁ ++ l₂

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ :
  a ∈ keys tail✝ → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tail✝ = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tail✝ = l₁ ++ l₂
h : a ∈ keys (head✝ :: tail✝)
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ head✝ :: tail✝ = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (head✝ :: tail✝) = l₁ ++ l₂
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : a ∈ keys l
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ l = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a l = l₁ ++ l₂
induction l
case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ :
  a ∈ keys tail✝ → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tail✝ = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tail✝ = l₁ ++ l₂
h : a ∈ keys (head✝ :: tail✝)
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ head✝ :: tail✝ = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (head✝ :: tail✝) = l₁ ++ l₂
case nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
h : a ∈ keys []
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ [] = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a [] = l₁ ++ l₂

case cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
tail_ih✝ :
  a ∈ keys tail✝ → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tail✝ = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tail✝ = l₁ ++ l₂
h : a ∈ keys (head✝ :: tail✝)
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ head✝ :: tail✝ = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (head✝ :: tail✝) = l₁ ++ l₂
case nil => cases h
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
h : a ∈ keys []
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ [] = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a [] = l₁ ++ l₂
cases h
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ keys (hd :: tl)
e : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ keys (hd :: tl)
e : ¬a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ keys (hd :: tl)
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
by_cases e : a = hd.1
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  hd.fst ∈ keys tl →
    ∃ b l₁ l₂, ¬hd.fst ∈ keys l₁ ∧ tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ keys (hd :: tl)
⊢ ∃ b l₁ l₂,
    ¬hd.fst ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst (hd :: tl) = l₁ ++ l₂
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ keys (hd :: tl)
e : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
subst e
no goals
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  hd.fst ∈ keys tl →
    ∃ b l₁ l₂, ¬hd.fst ∈ keys l₁ ∧ tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ keys (hd :: tl)
⊢ ∃ b l₁ l₂,
    ¬hd.fst ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst (hd :: tl) = l₁ ++ l₂
exact ⟨hd.2, [], tl, by simp, by cases hd; rfl, by simp⟩
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  hd.fst ∈ keys tl →
    ∃ b l₁ l₂, ¬hd.fst ∈ keys l₁ ∧ tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ keys (hd :: tl)
⊢ ¬hd.fst ∈ keys []
simp
case mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
tl : List (Sigma β)
fst✝ : α
snd✝ : β fst✝
ih :
  { fst := fst✝, snd := snd✝ }.fst ∈ keys tl →
    ∃ b l₁ l₂,
      ¬{ fst := fst✝, snd := snd✝ }.fst ∈ keys l₁ ∧
        tl = l₁ ++ { fst := { fst := fst✝, snd := snd✝ }.fst, snd := b } :: l₂ ∧
          kerase { fst := fst✝, snd := snd✝ }.fst tl = l₁ ++ l₂
h : { fst := fst✝, snd := snd✝ }.fst ∈ keys ({ fst := fst✝, snd := snd✝ } :: tl)
⊢ { fst := fst✝, snd := snd✝ } :: tl =
    [] ++ { fst := { fst := fst✝, snd := snd✝ }.fst, snd := { fst := fst✝, snd := snd✝ }.snd } :: tl
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  hd.fst ∈ keys tl →
    ∃ b l₁ l₂, ¬hd.fst ∈ keys l₁ ∧ tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ keys (hd :: tl)
⊢ hd :: tl = [] ++ { fst := hd.fst, snd := hd.snd } :: tl
cases hd
no goals
case mk
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
tl : List (Sigma β)
fst✝ : α
snd✝ : β fst✝
ih :
  { fst := fst✝, snd := snd✝ }.fst ∈ keys tl →
    ∃ b l₁ l₂,
      ¬{ fst := fst✝, snd := snd✝ }.fst ∈ keys l₁ ∧
        tl = l₁ ++ { fst := { fst := fst✝, snd := snd✝ }.fst, snd := b } :: l₂ ∧
          kerase { fst := fst✝, snd := snd✝ }.fst tl = l₁ ++ l₂
h : { fst := fst✝, snd := snd✝ }.fst ∈ keys ({ fst := fst✝, snd := snd✝ } :: tl)
⊢ { fst := fst✝, snd := snd✝ } :: tl =
    [] ++ { fst := { fst := fst✝, snd := snd✝ }.fst, snd := { fst := fst✝, snd := snd✝ }.snd } :: tl
rfl
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
hd : Sigma β
tl : List (Sigma β)
ih :
  hd.fst ∈ keys tl →
    ∃ b l₁ l₂, ¬hd.fst ∈ keys l₁ ∧ tl = l₁ ++ { fst := hd.fst, snd := b } :: l₂ ∧ kerase hd.fst tl = l₁ ++ l₂
h : hd.fst ∈ keys (hd :: tl)
⊢ kerase hd.fst (hd :: tl) = [] ++ tl
simp
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst ∨ a ∈ keys tl
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
h : a ∈ keys (hd :: tl)
e : ¬a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
simp at h
case neg.inl
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

case neg.inr
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst ∨ a ∈ keys tl
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
cases' h with h h
case neg.inr
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
case neg.inl
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

case neg.inr
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
exact absurd h e
case neg.inr.intro.intro.intro.intro.intro
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
case neg.inr
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩
no goals
case neg.inr.intro.intro.intro.intro.intro
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ hd :: tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂
exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁, by (rw [h₂]; rfl), by
      simp [e, h₃]⟩
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: tl = hd :: tl₁ ++ { fst := a, snd := b } :: tl₂
(rw [h₂]; rfl)
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ { fst := a, snd := b } :: tl₂) = hd :: tl₁ ++ { fst := a, snd := b } :: tl₂
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: tl = hd :: tl₁ ++ { fst := a, snd := b } :: tl₂
rw [h₂]
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ hd :: (tl₁ ++ { fst := a, snd := b } :: tl₂) = hd :: tl₁ ++ { fst := a, snd := b } :: tl₂
rfl
no goals
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ keys tl → ∃ b l₁ l₂, ¬a ∈ keys l₁ ∧ tl = l₁ ++ { fst := a, snd := b } :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a ∈ keys tl
b : β a
tl₁ tl₂ : List (Sigma β)
h₁ : ¬a ∈ keys tl₁
h₂ : tl = tl₁ ++ { fst := a, snd := b } :: tl₂
h₃ : kerase a tl = tl₁ ++ tl₂
⊢ kerase a (hd :: tl) = hd :: tl₁ ++ tl₂
simp [e, h₃]