no goals
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a✝ b a : α
⊢ Chain R a [] ↔ [] = [] ∨ Forall₂ R (a :: dropLast []) []
simp
no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
⊢ Chain R a (b :: l) ↔ b :: l = [] ∨ Forall₂ R (a :: dropLast (b :: l)) (b :: l)
by_cases h : l = [] <;>
simp [@chain_iff_forall₂ b l, *]