simp
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
nilP : ¬start = []
cancP : ¬List.getLast start nilP = (a, b)⁻¹
eqn : start :+ (a, b) = List.concat start (a, b)
nn : start :+ (a, b) ≠ []
cnc : start :+ (a, b) :+ (a, !b) = List.dropLast (start :+ (a, b)) :=
  nonnil_nextVertex_cancel (start :+ (a, b)) nn (a, !b)
    (of_eq_true
      ((congr
            (congrArg Eq
              (((fun {α} as as_1 e_as =>
                      Eq.rec (motive := fun as_2 e_as =>
                        ∀ (a : as ≠ []), List.getLast as a = List.getLast as_2 (e_as ▸ a))
                        (fun a => Eq.refl (List.getLast as a)) e_as)
                    (start :+ (a, b)) (start ++ [(a, b)]) (eqn.trans (List.concat_eq_append start (a, b))) nn).trans
                (List.getLast_append start (eqn.trans (List.concat_eq_append start (a, b)) ▸ nn))))
            (congrArg (Prod.mk a) (Bool.not_not b))).trans
        (eq_self (a, b))))
⊢ List.dropLast (List.concat start (a, b)) = start
no goals