law foldr_reverse_sym

bend-mathlib@0.8.1.0 · list.bend:3078

import Base

3078# A right fold over the reverse is a left fold with the arguments flipped, reversed to rewrite toward the simple side.
3079law foldr_reverse_sym:
3080  for ~a: Quant
3081  for ~A: Kind(a)
3082  for ~B: Type
3083  for ~f: A -> B -> B
3084  for xs: List<a, A>
3085  for -z: B
3086  {List.foldl(~a, ~A, ~B, ~(x => y => f(y, x)), xs, z) == List.foldr(~a, ~A, ~B, ~f, List.reverse(a, A, xs), z) : B}