Algebra.internal_foldl_eq_foldr: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/algebra.bend as Algebra
Lines 269-277 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=269&end_line=277

import Base

def internal_foldl_eq_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, +z: B, +xs: List<&2, B>) -> {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}:
  match xs:
    case Nil{}:
      {==}
    case +h <> +t:
      %comm(h, z) : {List.foldl(&2, B, B, op, t, _) == op(h, List.foldr(&2, B, B, op, t, z)) : B}
      %Equal.sym(B, List.foldl(&2, B, B, op, t, op(h, z)), op(h, List.foldl(&2, B, B, op, t, z)), internal_foldl_assoc(~B, ~op, ~assoc, t, h, z)) : {_ == op(h, List.foldr(&2, B, B, op, t, z)) : B}
      %internal_foldl_eq_foldr(~B, ~op, ~assoc, ~comm, z, t) : {op(h, List.foldl(&2, B, B, op, t, z)) == op(h, _) : 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_assoc