case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])

case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red L (reduce L)
induction' L with hd1 tl1 ih
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])

case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
case nil => constructor
no goals
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ Red [] (reduce [])
constructor
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (reduce tl1))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1) (reduce (hd1 :: tl1))
dsimp
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
⊢ Red tl1 (reduce tl1) →
    Red (hd1 :: tl1)
      (List.rec [hd1]
        (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
        (reduce tl1))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
ih : Red tl1 (reduce tl1)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (reduce tl1))
revert ih
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
⊢ Red tl1 TL →
    Red (hd1 :: tl1)
      (List.rec [hd1]
        (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) TL)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
⊢ Red tl1 (reduce tl1) →
    Red (hd1 :: tl1)
      (List.rec [hd1]
        (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
        (reduce tl1))
generalize htl : reduce tl1 = TL
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
ih : Red tl1 TL
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) TL)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
⊢ Red tl1 TL →
    Red (hd1 :: tl1)
      (List.rec [hd1]
        (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) TL)
intro ih
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) [])

case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 TL : List (α × Bool)
htl : reduce tl1 = TL
ih : Red tl1 TL
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) TL)
cases' TL with hd2 tl2
case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
case nil
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) [])

case cons
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
case nil => exact Red.cons_cons ih
no goals
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail) [])
exact Red.cons_cons ih
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1) (if hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd then tl2 else hd1 :: hd2 :: tl2)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1]
      (fun head tail tail_ih => if hd1.fst = head.fst ∧ hd1.snd = !head.snd then tail else hd1 :: head :: tail)
      (hd2 :: tl2))
dsimp only
case inl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd
⊢ Red (hd1 :: tl1) tl2

case inr
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1) (if hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd then tl2 else hd1 :: hd2 :: tl2)
split_ifs with h
case inl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd
⊢ Red (hd1 :: tl1) tl2
case inl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd
⊢ Red (hd1 :: tl1) tl2
trans
case inl.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
fst✝ : α
snd✝ : Bool
h : (fst✝, snd✝).fst = hd2.fst ∧ (fst✝, snd✝).snd = !hd2.snd
⊢ Red ((fst✝, snd✝) :: tl1) tl2
case inl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd
⊢ Red (hd1 :: tl1) tl2
cases hd1
case inl.mk.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
h : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd = !(fst✝, snd✝).snd
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
case inl.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
fst✝ : α
snd✝ : Bool
h : (fst✝, snd✝).fst = hd2.fst ∧ (fst✝, snd✝).snd = !hd2.snd
⊢ Red ((fst✝, snd✝) :: tl1) tl2
cases hd2
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
right✝ : (fst✝¹, snd✝¹).snd = !(fst✝, snd✝).snd
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
case inl.mk.mk
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
h : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst ∧ (fst✝¹, snd✝¹).snd = !(fst✝, snd✝).snd
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
cases h
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : fst✝¹ = fst✝
right✝ : snd✝¹ = !snd✝
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : (fst✝¹, snd✝¹).fst = (fst✝, snd✝).fst
right✝ : (fst✝¹, snd✝¹).snd = !(fst✝, snd✝).snd
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
dsimp at *
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
⊢ Red ((fst✝, !snd✝) :: tl1) tl2
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝¹ : α
snd✝¹ : Bool
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
left✝ : fst✝¹ = fst✝
right✝ : snd✝¹ = !snd✝
⊢ Red ((fst✝¹, snd✝¹) :: tl1) tl2
subst_vars
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
⊢ Red ((fst✝, !snd✝) :: (fst✝, snd✝) :: tl2) tl2
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
⊢ Red ((fst✝, !snd✝) :: tl1) tl2
apply Red.trans (Red.cons_cons ih)
no goals
case inl.mk.mk.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
tl1 tl2 : List (α × Bool)
fst✝ : α
snd✝ : Bool
htl : reduce tl1 = (fst✝, snd✝) :: tl2
ih : Red tl1 ((fst✝, snd✝) :: tl2)
⊢ Red ((fst✝, !snd✝) :: (fst✝, snd✝) :: tl2) tl2
exact Red.Step.cons_not_rev.to_red
no goals
case inr
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.fst = hd2.fst ∧ hd1.snd = !hd2.snd)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)
exact Red.cons_cons ih