ProofFastW1.uand_assoc: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_w1.bend as ProofFastW1
Lines 39-43 of lawful-bytes@0.1.1.0/proof_fast_w1.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_w1.bend&start_line=39&end_line=43

import Base

law uand_assoc:
  for +a: U32
  for +b: U32
  for +c: U32
  {U32.and(a, U32.and(b, c)) == U32.and(U32.and(a, b), c) : U32}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_w1.bend&name=wand_assoc