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

import Base

# Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.
law op_assoc4_sym:
  for ~A: Data
  for ~op: A -> A -> A
  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
  for +a: A
  for +b: A
  for +c: A
  for +d: A
  {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_assoc4