let (a, b) := letter
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
cancP : List.getLast start nilP = letter⁻¹
⊢ start ++ [letter] ∼ List.dropLast start
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
a : α
b : Bool
cancP : List.getLast start nilP = (a, b)⁻¹
⊢ start ++ [(a, b)] ∼ List.dropLast start