apply reduced_start (L₁ ++ L₂')
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ False
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
letter : α × Bool
reduced_start : Reduced start
nilP : ¬start = []
L' : List (α × Bool)
step : Step (start :+ letter) L'
x : α
b : Bool
L₁ L₂ : List (α × Bool)
eqs : start :+ letter = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
cancP : List.getLast start nilP = letter⁻¹
eq1 : List.dropLast start = L₁ ++ (x, b) :: (x, !b) :: L₂
eq1' : start = L₁ ++ (x, b) :: (x, !b) :: (L₂ ++ [List.getLast start nilP])
L₂' : List (α × Bool) := L₂ ++ [List.getLast start nilP]
⊢ Step start (L₁ ++ L₂')