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 ∈ L.sections ↔ List.Forall₂ (fun (x1 : α) (x2 : List α) => x1 ∈ x2) f L

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

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