English
For any relation r, the operation sections is compatible with the Forall₂ lifting: if two lists of lists L and L' are related by Forall₂ (Forall₂ r), then their sections are related by Forall₂ (Forall₂ r).
Русский
Для любой связи r операция sections согласуется с подстановкой Forall₂: если два списка списков L и L' связаны Forall₂ (Forall₂ r), то их секции связаны Forall₂ (Forall₂ r).
LaTeX
$$$ \\forall r : \\alpha \\rightarrow \\beta \\rightarrow \\mathrm{Prop},\\; \\forall L,L' : \\ List (List \\alpha),\\; (\\mathrm{Forall_2}\\ (\\mathrm{Forall_2}\\ r) \\; L\\; L') \\Rightarrow (\\mathrm{Forall_2}\\ (\\mathrm{Forall_2}\\ r) (\\mathrm{sections}(L)) (\\mathrm{sections}(L'))).$$$
Lean4
theorem rel_sections {r : α → β → Prop} : (Forall₂ (Forall₂ r) ⇒ Forall₂ (Forall₂ r)) sections sections
| _, _, Forall₂.nil => Forall₂.cons Forall₂.nil Forall₂.nil
| _, _, Forall₂.cons h₀ h₁ =>
rel_flatMap (rel_sections h₁) fun _ _ hl => rel_map (fun _ _ ha => Forall₂.cons ha hl) h₀
