simp [nextVertex,  eql, if_pos, nonnil]
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
nonnil : start ≠ []
letter : α × Bool
eql : List.getLast start nonnil = letter⁻¹
⊢ start :+ letter = List.dropLast start
no goals