simp [cancP, nonnil_nextVertex_extend, nilP]
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
nilP : ¬start = []
cancP : ¬List.getLast start nilP = letter⁻¹
⊢ List.concat start letter ∼ start :+ letter
no goals