α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
⊢ Red L [(x, !b)]
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]
have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]
let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]
rw [singleton_iff] at h₁
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]
subst L'
no goals
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]
assumption