case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)

case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)
by_cases h : a = a'
case neg.nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
⊢ kerase a (kerase a' []) = kerase a' (kerase a [])

case neg.cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
case neg
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : ¬a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)
induction' l with x xs
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
l : List (Sigma β)
h : a = a'
⊢ kerase a (kerase a' l) = kerase a' (kerase a l)
subst a'
no goals
case pos
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ kerase a (kerase a l) = kerase a (kerase a l)
rfl
no goals
case neg.nil
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
⊢ kerase a (kerase a' []) = kerase a' (kerase a [])
rfl
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : ¬a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
case neg.cons
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
by_cases a' = x.1
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))

case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : ¬a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
by_cases h' : a = x.1
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
h : ¬a = x.fst
tail_ih✝ : kerase a (kerase x.fst xs) = kerase x.fst (kerase a xs)
⊢ kerase a (kerase x.fst (x :: xs)) = kerase x.fst (kerase a (x :: xs))
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : a' = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
subst a'
no goals
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
h : ¬a = x.fst
tail_ih✝ : kerase a (kerase x.fst xs) = kerase x.fst (kerase a xs)
⊢ kerase a (kerase x.fst (x :: xs)) = kerase x.fst (kerase a (x :: xs))
simp [kerase_cons_ne h, kerase_cons_eq rfl]
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h✝ : ¬a' = x.fst
h : ¬x.fst = a'
tail_ih✝ : kerase x.fst (kerase a' xs) = kerase a' (kerase x.fst xs)
⊢ kerase x.fst (kerase a' (x :: xs)) = kerase a' (kerase x.fst (x :: xs))
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : ¬a' = x.fst
h' : a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
subst a
no goals
case pos
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a' : α
x : Sigma β
xs : List (Sigma β)
h✝ : ¬a' = x.fst
h : ¬x.fst = a'
tail_ih✝ : kerase x.fst (kerase a' xs) = kerase a' (kerase x.fst xs)
⊢ kerase x.fst (kerase a' (x :: xs)) = kerase a' (kerase x.fst (x :: xs))
simp [kerase_cons_eq rfl, kerase_cons_ne (Ne.symm h)]
no goals
case neg
α : Type u
β : α → Type v
l l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
h✝ : ¬a = a'
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : kerase a (kerase a' xs) = kerase a' (kerase a xs)
h : ¬a' = x.fst
h' : ¬a = x.fst
⊢ kerase a (kerase a' (x :: xs)) = kerase a' (kerase a (x :: xs))
simp [kerase_cons_ne, *]