α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b x : α
l : List α
y : α
h : Chain' R (x :: y :: List.tail l)
hy : y ∈ head? l
⊢ R x y
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b x : α
l : List α
h : Chain' R (x :: l)
y : α
hy : y ∈ head? l
⊢ R x y
rw [← cons_head?_tail hy] at h
no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b x : α
l : List α
y : α
h : Chain' R (x :: y :: List.tail l)
hy : y ∈ head? l
⊢ R x y
exact h.rel_head