law foldl_append_sym

bend-mathlib@0.8.1.0 · list.bend:2469

import Base

2469# A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.
2470law foldl_append_sym:
2471  for ~a: Quant
2472  for ~A: Kind(a)
2473  for ~B: Type
2474  for ~f: B -> A -> B
2475  for xs: List<a, A>
2476  for -ys: List<a, A>
2477  for -z: B
2478  {List.foldl(~a, ~A, ~B, ~f, ys, List.foldl(~a, ~A, ~B, ~f, xs, z)) == List.foldl(~a, ~A, ~B, ~f, List.append(a, A, xs, ys), z) : B}