intro reduced_start
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
⊢ Reduced start → Reduced (start :+ letter)
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
⊢ Reduced (start :+ letter)