apply reduced_start
case h
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ False
case h.a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ Step start ?h.L'

case h.L'
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : List.getLast start nilP = (a, b)⁻¹
nil' : ¬List.dropLast start = []
cancP' : List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
sp' : List.dropLast (List.dropLast start) ++ [List.getLast (List.dropLast start) nil'] = List.dropLast start :=
  split_drop (List.dropLast start) nil'
L' : List (α × Bool) := List.dropLast (List.dropLast start)
sp : L' ++ [(a, b), (a, !b)] = start
this : List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ [(a, b), (a, !b)]
step : Step start (L' ++ [])
⊢ List (α × Bool)