α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (a :: l)
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain R a l
suffices Chain' R (a::l) by
  assumption
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (destutter' R a l)
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (a :: l)
rw [← h]
no goals
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (destutter' R a l)
exact l.destutter'_is_chain' R a
no goals
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
this : Chain' R (a :: l)
⊢ Chain R a l
assumption