Lemmas about Chain' and OfFn

This file provides lemmas involving both List.Chain' and List.OfFn.

theorem List.chain'_ofFn {α : Type u_1} {n : ℕ} {f : Fin n → α} {r : α → α → Prop} : List.Chain' r (List.ofFn f) ↔ ∀ (i : ℕ) (hi : i + 1 < n), r (f ⟨i, ⋯⟩) (f ⟨i + 1, hi⟩)