match word with
| [] => simp [finalVertex]
| head ::tail => 
  simp [finalVertex, List.foldl_cons]
  let ih := finalVertex_homotopic_append (start :+ head) tail
  simp [finalVertex, List.foldl_cons] at ih
  let eqn := nextVertex_homotopic_concat start head
  show mk (start ++ head :: tail) = mk (List.foldl nextVertex (start :+ head) tail)
  rw [←ih]
  let eqn' := append_homotopic tail eqn
  simp [← eqn']
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
⊢ start ++ word ∼ finalVertex start word
no goals