no goals
α : Type u_1
R : α → α → Prop
a b : α
l : List α
p : Chain R a (b :: l)
⊢ R a b ∧ Chain R b l
cases p with | cons n p => exact ⟨n, p⟩
no goals
case cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
n : R a b
p : Chain R b l
⊢ R a b ∧ Chain R b l
exact ⟨n, p⟩