α : Type u
L L₁ L₂ L₃ L₄ L' : List (α × Bool)
h' : [] = L'
⊢ ¬Step L' L
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ¬Step [] L
generalize h' : [] = L'
α : Type u
L L₁ L₂ L₃ L₄ L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False
α : Type u
L L₁ L₂ L₃ L₄ L' : List (α × Bool)
h' : [] = L'
⊢ ¬Step L' L
intro h
case not
α : Type u
L₁✝ L₂✝ L₃ L₄ L₁ L₂ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂
⊢ False
α : Type u
L L₁ L₂ L₃ L₄ L' : List (α × Bool)
h' : [] = L'
h : Step L' L
⊢ False
cases' h with L₁ L₂
no goals
case not
α : Type u
L₁✝ L₂✝ L₃ L₄ L₁ L₂ : List (α × Bool)
x✝ : α
b✝ : Bool
h' : [] = L₁ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂
⊢ False
simp [List.nil_eq_append] at h'