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