List sections

This file proves some stuff about List.sections (definition in Data.List.Defs). A section of a list of lists [l₁, ..., lₙ] is a list whose i-th element comes from the i-th list.

theorem List.mem_sections {α : Type u_1} {L : List (List α)} {f : List α} : f ∈ List.sections L ↔ List.Forall₂ (fun (x : α) (x_1 : List α) => x ∈ x_1) f L

theorem List.mem_sections_length {α : Type u_1} {L : List (List α)} {f : List α} (h : f ∈ List.sections L) : List.length f = List.length L

theorem List.rel_sections {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : (List.Forall₂ (List.Forall₂ r) ⇒ List.Forall₂ (List.Forall₂ r)) List.sections List.sections