rw [←ih]
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ List.foldl nextVertex (start :+ head) tail :=
  finalVertex_homotopic_append (start :+ head) tail
eqn : List.concat start head ∼ start :+ head := nextVertex_homotopic_concat start head
⊢ mk (start ++ head :: tail) = mk (start :+ head ++ tail)