intro reduced_start
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
⊢ Reduced start → start :+ (a, b) :+ (a, !b) = start
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
a : α
b : Bool
reduced_start : Reduced start
⊢ start :+ (a, b) :+ (a, !b) = start