if nilP: start = [] 
then 
  simp [nil_nextVertex, nilP]
  apply reduced_singleton
else
  intro L' step
  let ⟨x, b, L₁, L₂, eqs⟩ := exists_of_step step
  let eq1 := eqs.1
  if cancP:start.getLast nilP = letter⁻¹ 
  then 
    simp [cancP, nilP, nonnil_nextVertex_cancel] at eq1
    have eq1' : start.dropLast.concat (start.getLast nilP) = 
        (L₁ ++ (x, b) :: (x, !b) :: L₂).concat (start.getLast nilP) :=
      by rw [eq1]
    simp [split_drop, nilP] at eq1'
    let L₂' := L₂ ++ [start.getLast nilP]
    apply reduced_start (L₁ ++ L₂')
    rw [eq1']
    apply Step.not
  else 
    simp [cancP, nilP, nonnil_nextVertex_extend] at eq1
    if endP : L₂ = [] 
    then
      simp [endP] at eq1
      rw [←List.concat_eq_append] at eq1
      have : L₁ ++ [(x, b), (x, !b)] = 
        (L₁ ++ [(x, b)]).concat (x, !b) := by simp
      rw [this] at eq1
      let eq1' := List.of_concat_eq_concat eq1
      let eq1'' := eq1'.1
      let sp := split_drop start nilP
      rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
      let eq1''' := eq1'.2
      let eq2' := List.of_concat_eq_concat eq1''
      let _eq2'' := eq2'.2
      rw [eq1''', _eq2''] at cancP
      simp [inv_def] at cancP
    else
      rw [← split_drop L₂ endP] at eq1
      rw [← List.cons_append, ← List.cons_append, 
        ← List.append_assoc, ← List.concat_eq_append,
        ← List.concat_eq_append] at eq1
      let eq1' := List.of_concat_eq_concat eq1
      let eq1'' := eq1'.1
      apply reduced_start (L₁ ++ L₂.dropLast)
      rw [eq1'']
      apply Step.not
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
⊢ Reduced (start :+ letter)
no goals