rw [← sp, ←List.concat_eq_append, ←List.concat_eq_append] at eq1''
α : 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⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : start = L₁ ++ [(x, b)] := eq1'.left
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop 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⁻¹
endP : L₂ = []
eq1 : List.concat start letter = List.concat (L₁ ++ [(x, b)]) (x, !b)
this : L₁ ++ [(x, b), (x, !b)] = List.concat (L₁ ++ [(x, b)]) (x, !b)
eq1' : start = L₁ ++ [(x, b)] ∧ letter = (x, !b) := List.of_concat_eq_concat eq1
eq1'' : List.concat (List.dropLast start) (List.getLast start nilP) = List.concat L₁ (x, b)
sp : List.dropLast start ++ [List.getLast start nilP] = start := split_drop start nilP
⊢ False