if nilP: start = [] then
  simp [nilP, nil_nextVertex]
else
  if cancP:start.getLast nilP = letter⁻¹
  then
    simp [cancP, nonnil_nextVertex_cancel, nilP]
    let (a, b) := letter
    apply Quot.sound
    let sp := split_drop start nilP
    rw [cancP] at sp
    let step' := @Step.not _ start.dropLast ([]) a !b
    simp [Bool.not_not] at step'
    have : List.dropLast start ++ [(a, !b), (a, b)] = 
      start.dropLast ++ [(a, !b)] ++ [(a, b)] := by simp
    rw [inv_def] at sp
    rw [this, sp] at step'
    exact step'
  else
    simp [cancP, nonnil_nextVertex_extend, nilP]
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
⊢ List.concat start letter ∼ start :+ letter
no goals