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 ↔ 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} : Relator.LiftFun (Forall₂ (Forall₂ r)) (Forall₂ (Forall₂ r)) sections sections