intro step
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
⊢ Step L L' → ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂
α : Type
inst✝ : DecidableEq α
L L' : List (α × Bool)
step : Step L L'
⊢ ∃ x b L₁ L₂, L = L₁ ++ (x, b) :: (x, !b) :: L₂ ∧ L' = L₁ ++ L₂