Algebra.foldl_op_eq_foldr_op: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/algebra.bend as Algebra
Lines 242-251 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=242&end_line=251

import Base

# Folding left equals folding right for an associative, commutative operation with a left identity (foldl_eq_foldr needs no identity).
law foldl_op_eq_foldr_op:
  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 ~id: @x: B -> {op(z, x) == x : B}
  for +xs: List<&2, B>
  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_foldr