simp [nilP, nil', nil_nextVertex]
α : 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 = []
⊢ List.dropLast start :+ (a, !b) = start
α : 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 = []
⊢ [(a, !b)] = start