law foldr_append

bend-mathlib@0.8.1.0 · list.bend:141

import Base

141# A right fold over an append folds the first part onto the fold of the second.
142law foldr_append:
143  for ~a: Quant
144  for ~A: Kind(a)
145  for ~B: Type
146  for ~f: A -> B -> B
147  for xs: List<a, A>
148  for -ys: List<a, A>
149  for -z: B
150  {List.foldr(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) == List.foldr(~a, ~A, ~B, ~f, xs, List.foldr(~a, ~A, ~B, ~f, ys, z)) : B}