if nilP: start = [] then
  simp [nilP, nextVertex, inv_def]
else 
  if cancP:start.getLast nilP = (a, b)⁻¹ 
  then 
    simp [cancP, nonnil_nextVertex_cancel, nilP]
    if nil' : start.dropLast = [] 
    then
      simp [nilP, nil', nil_nextVertex]
      let sp := split_drop start nilP
      rw [←sp, nil']
      simp
      simp [inv_def] at cancP
      rw [cancP]
    else
      if cancP':start.dropLast.getLast nil'  = (a, !b)⁻¹ 
      then
        let sp := split_drop start nilP
        let sp' := split_drop start.dropLast nil'
        rw [←sp', cancP', cancP] at sp
        simp [inv_def' a !b] at sp
        let L' := start.dropLast.dropLast
        have : 
          List.dropLast (List.dropLast start) ++ [(a, b), (a, b)⁻¹] = L' ++ (a, b) :: (a, !b) :: [] := by simp [inv_def]
        rw [this] at sp
        have step : Step start (L' ++ []) := by
          rw [← sp]
          show Step (L' ++ (a, b) :: (a, !b) :: []) (L' ++ [])
          apply Step.not
        apply False.elim
        apply reduced_start
        exact step
      else
        let res := 
          nonnil_nextVertex_extend start.dropLast nil' (a, !b) cancP'    
        rw [res]
        let sp := split_drop start nilP
        rw [cancP] at sp
        simp [inv_def] at cancP
        simp [inv_def] at sp 
        simp [sp]
  else
    have eqn : start :+ (a, b) = start.concat (a, b) := by 
      simp [nonnil_nextVertex_extend, cancP, nilP]
    have nn : start :+ (a, b) ≠ [] := by 
      simp [eqn]
    let cnc := 
      nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
      (by 
        simp [inv_def, cancP, eqn]) 
    rw [cnc, eqn]
    simp
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
⊢ start :+ (a, b) :+ (a, !b) = start
no goals