Algebra.foldl_eq_foldr: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/algebra.bend as Algebra
Lines 279-287 of bend-mathlib@0.8.1.0/algebra.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/algebra.bend&start_line=279&end_line=287

import Base

# Folding left equals folding right for an associative, commutative operation (Mathlib's List.foldl_eq_foldr).
law foldl_eq_foldr:
  for ~B: Data
  for ~op: B -> B -> B
  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
  for +z: B
  for +xs: List<&2, B>
  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.foldl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.foldr
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_foldl_eq_foldr