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
nilP : ¬start = []
⊢ start :+ (a, b) :+ (a, !b) = start
no goals