English
There is a lifting of Forall₂ through foldl, i.e., if a relation P is closed under a step given by R, then folding with R preserves P.
Русский
Существует подъем Forall₂ через foldl: если отношение P сохраняется при шаге, заданном R, то свертка через foldl сохраняет P.
LaTeX
$$$ \mathrm{rel\_foldl} : ((P \Rightarrow R \Rightarrow P) \Rightarrow P \Rightarrow Forall₂ R \Rightarrow P)\ \mathrm{foldl}\ \mathrm{foldl}$$$
Lean4
theorem rel_foldl : ((P ⇒ R ⇒ P) ⇒ P ⇒ Forall₂ R ⇒ P) foldl foldl
| _, _, _, _, _, h, _, _, Forall₂.nil => h
| _, _, hfg, _, _, hxy, _, _, Forall₂.cons hab hs => rel_foldl (@hfg) (hfg hxy hab) hs
