rw [cancP] at sp
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ Step (start ++ [(a, b)]) (List.dropLast start)
case a
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
sp : List.dropLast start ++ [(a, b)⁻¹] = start
⊢ Step (start ++ [(a, b)]) (List.dropLast start)