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)⁻¹
nil' : ¬List.dropLast start = []
⊢ List.dropLast start :+ (a, !b) = start
no goals