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 (x : α) (x_1 : List α) => x x_1) 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