let res := 
  nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'
α : 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 = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
⊢ 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 = []
cancP' : ¬List.getLast (List.dropLast start) nil' = (a, !b)⁻¹
res : List.dropLast start :+ (a, !b) = List.concat (List.dropLast start) (a, !b) :=
  nonnil_nextVertex_extend (List.dropLast start) nil' (a, !b) cancP'
⊢ List.dropLast start :+ (a, !b) = start