case h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ Red [(x1, !b1), (x2, b2)] L ↔ L = [(x1, !b1), (x2, b2)]
apply reflTransGen_iff_eq
case h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
⊢ ∀ (b : List (α × Bool)), ¬Step L' b
case h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
⊢ ∀ (b : List (α × Bool)), ¬Step [(x1, !b1), (x2, b2)] b
generalize eq : [(x1, not b1), (x2, b2)] = L'
case h
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
L : List (α × Bool)
h' : Step L' L
⊢ False
case h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
⊢ ∀ (b : List (α × Bool)), ¬Step L' b
intro L h'
case h.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : [(x1, !b1), (x2, b2)] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False
case h
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
L : List (α × Bool)
h' : Step L' L
⊢ False
cases h'
case h.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : L₁✝ = [] ∧ (x✝ = x1 ∧ b✝ = !b1) ∧ (x✝ = x2 ∧ (!b✝) = b2) ∧ L₂✝ = []
⊢ False
case h.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : [(x1, !b1), (x2, b2)] = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ False
simp [List.cons_eq_append_iff, List.nil_eq_append] at eq
case h.not.intro.intro.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
case h.not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
eq : L₁✝ = [] ∧ (x✝ = x1 ∧ b✝ = !b1) ∧ (x✝ = x2 ∧ (!b✝) = b2) ∧ L₂✝ = []
⊢ False
rcases eq with ⟨rfl, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl⟩
case h.not.intro.intro.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
case h.not.intro.intro.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
subst_vars
no goals
case h.not.intro.intro.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
b1 : Bool
x✝ : α
h : (x✝, b1) ≠ (x✝, !!b1)
⊢ False
simp at h