law op_four_sym

bend-mathlib@0.8.1.0 · algebra.bend:336

import Base

336# Middle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.
337law op_four_sym:
338  for ~A: Data
339  for ~op: A -> A -> A
340  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
341  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
342  for +a: A
343  for +b: A
344  for +c: A
345  for +d: A
346  {op(op(a, c), op(b, d)) == op(op(a, b), op(c, d)) : A}