let ih := finalVertex_homotopic_append (start :+ head) tail
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
ih : start :+ head ++ tail ∼ finalVertex (start :+ head) tail := finalVertex_homotopic_append (start :+ head) tail
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail