have eqn : start :+ (a, b) = start.concat (a, b) := by 
  simp [nonnil_nextVertex_extend, cancP, nilP]
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
⊢ start :+ (a, b) :+ (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)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
⊢ start :+ (a, b) :+ (a, !b) = start