no goals
α : Type u
β : Type v
R r : α → α → Prop
l l₁ l₂ : List α
a✝ b a : α
⊢ Chain' R (reverse [a]) ↔ Chain' (flip R) [a]
simp only [chain'_singleton, reverse_singleton]
no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ a b : α
l : List α
⊢ Chain' R (reverse (a :: b :: l)) ↔ Chain' (flip R) (a :: b :: l)
rw [chain'_cons, reverse_cons, reverse_cons, append_assoc, cons_append, nil_append,
  chain'_split, ← reverse_cons, @chain'_reverse (b :: l), and_comm, chain'_pair, flip]