simp [nil_nextVertex, nilP]
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced (start :+ letter)
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : start = []
⊢ Reduced [letter]