case refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce L₁ = reduce L₁

case tail
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
L1 L' : List (α × Bool)
L2 : ReflTransGen Red.Step (reduce L₁) L1
H1 : Red.Step L1 L'
H2 : reduce L₁ = L1
⊢ reduce L₁ = L'
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
H : Red (reduce L₁) L₂
⊢ reduce L₁ = L₂
induction' H with L1 L' L2 H1 H2 ih
no goals
case refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce L₁ = reduce L₁
rfl
case tail.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
L4 L5 : List (α × Bool)
x : α
b : Bool
L2 : ReflTransGen Red.Step (reduce L₁) (L4 ++ (x, b) :: (x, !b) :: L5)
H2 : reduce L₁ = L4 ++ (x, b) :: (x, !b) :: L5
⊢ reduce L₁ = L4 ++ L5
case tail
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
L1 L' : List (α × Bool)
L2 : ReflTransGen Red.Step (reduce L₁) L1
H1 : Red.Step L1 L'
H2 : reduce L₁ = L1
⊢ reduce L₁ = L'
cases' H1 with L4 L5 x b
no goals
case tail.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
L4 L5 : List (α × Bool)
x : α
b : Bool
L2 : ReflTransGen Red.Step (reduce L₁) (L4 ++ (x, b) :: (x, !b) :: L5)
H2 : reduce L₁ = L4 ++ (x, b) :: (x, !b) :: L5
⊢ reduce L₁ = L4 ++ L5
exact reduce.not H2