induction step with
| @not L₁ L₂ x b =>  use x, b, 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₂
no goals