simp [finalVertex, List.foldl_cons]
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ finalVertex start (head :: tail)
α : Type
inst✝ : DecidableEq α
start word : List (α × Bool)
head : α × Bool
tail : List (α × Bool)
⊢ start ++ head :: tail ∼ List.foldl nextVertex (start :+ head) tail