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
nilP : ¬start = []
⊢ List.concat start letter ∼ start :+ letter
no goals