α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
⊢ Red (p :: L₁) (p :: L₂) → Red L₁ L₂
generalize eq₁ : (p :: L₁ : List _) = LL₁
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
⊢ Red LL₁ LL₂ → Red L₁ L₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂
generalize eq₂ : (p :: L₂ : List _) = LL₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
⊢ Red L₁ L₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
⊢ Red LL₁ LL₂ → Red L₁ L₂
intro h
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁✝ : p :: L₁✝ = LL₁
LL₂ : List (α × Bool)
eq₂✝ : p :: L₂✝ = LL₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

case head
α : Type u
L L₁✝¹ L₂✝¹ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁✝ : p :: L₁✝¹ = LL₁
LL₂ : List (α × Bool)
eq₂✝ : p :: L₂✝¹ = LL₂
L₁✝ L₂✝ : List (α × Bool)
h₁₂ : Step L₁✝ L₂✝
h : ReflTransGen Step L₂✝ LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = LL₂ → Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = L₁✝
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
h : Red LL₁ LL₂
⊢ Red L₁ L₂
induction' h using Relation.ReflTransGen.head_induction_on
  with L₁ L₂ h₁₂ h ih
  generalizing L₁ L₂
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = p :: L₂✝
eq₂ : p :: L₂ = p :: L₂✝
⊢ Red L₁ L₂
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁✝ : p :: L₁✝ = LL₁
LL₂ : List (α × Bool)
eq₂✝ : p :: L₂✝ = LL₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂
subst_vars
case refl.refl
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
L₁ : List (α × Bool)
eq₁ : p :: L₁ = p :: L₂
⊢ Red L₁ L₂
case refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = p :: L₂✝
eq₂ : p :: L₂ = p :: L₂✝
⊢ Red L₁ L₂
cases eq₂
case refl.refl.refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
⊢ Red L₂ L₂
case refl.refl
α : Type u
L L₁✝ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
L₁ : List (α × Bool)
eq₁ : p :: L₁ = p :: L₂
⊢ Red L₁ L₂
cases eq₁
no goals
case refl.refl.refl
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
p : α × Bool
⊢ Red L₂ L₂
constructor
case head
α : Type u
L L₁✝ L₂✝¹ L₃ L₄ : List (α × Bool)
p : α × Bool
L₂✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step L₂✝ (p :: L₂✝¹)
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = p :: L₂✝¹ → Red L₁ L₂
eq₂ : p :: L₂ = p :: L₂✝¹
h₁₂ : Step (p :: L₁) L₂✝
⊢ Red L₁ L₂
case head
α : Type u
L L₁✝¹ L₂✝¹ L₃ L₄ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁✝ : p :: L₁✝¹ = LL₁
LL₂ : List (α × Bool)
eq₂✝ : p :: L₂✝¹ = LL₂
L₁✝ L₂✝ : List (α × Bool)
h₁₂ : Step L₁✝ L₂✝
h : ReflTransGen Step L₂✝ LL₂
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = LL₂ → Red L₁ L₂
L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = L₁✝
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂
subst_vars
case head.refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
L₂ L₁ : List (α × Bool)
h : ReflTransGen Step L₂ (p :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, p :: L₁ = L₂ → p :: L₂_1 = p :: L₂✝ → Red L₁ L₂_1
h₁₂ : Step (p :: L₁) L₂
⊢ Red L₁ L₂✝
case head
α : Type u
L L₁✝ L₂✝¹ L₃ L₄ : List (α × Bool)
p : α × Bool
L₂✝ L₁ L₂ : List (α × Bool)
h : ReflTransGen Step L₂✝ (p :: L₂✝¹)
ih : ∀ {L₁ L₂ : List (α × Bool)}, p :: L₁ = L₂✝ → p :: L₂ = p :: L₂✝¹ → Red L₁ L₂
eq₂ : p :: L₂ = p :: L₂✝¹
h₁₂ : Step (p :: L₁) L₂✝
⊢ Red L₁ L₂
cases eq₂
case head.refl.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₂ L₁ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂ ((a, b) :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂ → (a, b) :: L₂_1 = (a, b) :: L₂✝ → Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) L₂
⊢ Red L₁ L₂✝
case head.refl
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
p : α × Bool
L₂ L₁ : List (α × Bool)
h : ReflTransGen Step L₂ (p :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, p :: L₁ = L₂ → p :: L₂_1 = p :: L₂✝ → Red L₁ L₂_1
h₁₂ : Step (p :: L₁) L₂
⊢ Red L₁ L₂✝
cases' p with a b
case head.refl.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₂ L₁ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂ ((a, b) :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂ → (a, b) :: L₂_1 = (a, b) :: L₂✝ → Red L₁ L₂_1
h₁₂ : (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
⊢ Red L₁ L₂✝
case head.refl.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₂ L₁ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂ ((a, b) :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂ → (a, b) :: L₂_1 = (a, b) :: L₂✝ → Red L₁ L₂_1
h₁₂ : Step ((a, b) :: L₁) L₂
⊢ Red L₁ L₂✝
rw [Step.cons_left_iff] at h₁₂
case head.refl.mk.inl.intro.intro
α : Type u
L✝ L₁✝ L₂ L₃ L₄ L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h₁₂ : Step L₁ L
h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = (a, b) :: L → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red L₁ L₂

case head.refl.mk.inr
α : Type u
L L₁ L₂✝ L₃ L₄ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂ ((a, b) :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂ → (a, b) :: L₂_1 = (a, b) :: L₂✝ → Red L₁ L₂_1
⊢ Red ((a, !b) :: L₂) L₂✝
case head.refl.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ L₂ L₁ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂ ((a, b) :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂ → (a, b) :: L₂_1 = (a, b) :: L₂✝ → Red L₁ L₂_1
h₁₂ : (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
⊢ Red L₁ L₂✝
rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)
no goals
case head.refl.mk.inl.intro.intro
α : Type u
L✝ L₁✝ L₂ L₃ L₄ L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h₁₂ : Step L₁ L
h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = (a, b) :: L → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red L₁ L₂
exact (ih rfl rfl).head h₁₂
no goals
case head.refl.mk.inr
α : Type u
L L₁ L₂✝ L₃ L₄ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step L₂ ((a, b) :: L₂✝)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = L₂ → (a, b) :: L₂_1 = (a, b) :: L₂✝ → Red L₁ L₂_1
⊢ Red ((a, !b) :: L₂) L₂✝
exact (cons_cons h).tail Step.cons_not_rev