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

import Base

# Three-way commutation from commutativity alone.
law op_comm3:
  for ~A: Data
  for ~op: A -> A -> A
  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
  for +a: A
  for +b: A
  for +c: A
  {op(op(a, b), c) == op(c, op(b, a)) : A}

Uses (1):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym