Bytes.bits32: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend as Bytes
Lines 10-108 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend&start_line=10&end_line=108

import Base

# Two words are equal when their digits are.
law bits32:
  for -y0: Bool
  for -y1: Bool
  for -y2: Bool
  for -y3: Bool
  for -y4: Bool
  for -y5: Bool
  for -y6: Bool
  for -y7: Bool
  for -y8: Bool
  for -y9: Bool
  for -y10: Bool
  for -y11: Bool
  for -y12: Bool
  for -y13: Bool
  for -y14: Bool
  for -y15: Bool
  for -y16: Bool
  for -y17: Bool
  for -y18: Bool
  for -y19: Bool
  for -y20: Bool
  for -y21: Bool
  for -y22: Bool
  for -y23: Bool
  for -y24: Bool
  for -y25: Bool
  for -y26: Bool
  for -y27: Bool
  for -y28: Bool
  for -y29: Bool
  for -y30: Bool
  for -y31: Bool
  for -z0: Bool
  for -z1: Bool
  for -z2: Bool
  for -z3: Bool
  for -z4: Bool
  for -z5: Bool
  for -z6: Bool
  for -z7: Bool
  for -z8: Bool
  for -z9: Bool
  for -z10: Bool
  for -z11: Bool
  for -z12: Bool
  for -z13: Bool
  for -z14: Bool
  for -z15: Bool
  for -z16: Bool
  for -z17: Bool
  for -z18: Bool
  for -z19: Bool
  for -z20: Bool
  for -z21: Bool
  for -z22: Bool
  for -z23: Bool
  for -z24: Bool
  for -z25: Bool
  for -z26: Bool
  for -z27: Bool
  for -z28: Bool
  for -z29: Bool
  for -z30: Bool
  for -z31: Bool
  for e0: {y0 == z0 : Bool}
  for e1: {y1 == z1 : Bool}
  for e2: {y2 == z2 : Bool}
  for e3: {y3 == z3 : Bool}
  for e4: {y4 == z4 : Bool}
  for e5: {y5 == z5 : Bool}
  for e6: {y6 == z6 : Bool}
  for e7: {y7 == z7 : Bool}
  for e8: {y8 == z8 : Bool}
  for e9: {y9 == z9 : Bool}
  for e10: {y10 == z10 : Bool}
  for e11: {y11 == z11 : Bool}
  for e12: {y12 == z12 : Bool}
  for e13: {y13 == z13 : Bool}
  for e14: {y14 == z14 : Bool}
  for e15: {y15 == z15 : Bool}
  for e16: {y16 == z16 : Bool}
  for e17: {y17 == z17 : Bool}
  for e18: {y18 == z18 : Bool}
  for e19: {y19 == z19 : Bool}
  for e20: {y20 == z20 : Bool}
  for e21: {y21 == z21 : Bool}
  for e22: {y22 == z22 : Bool}
  for e23: {y23 == z23 : Bool}
  for e24: {y24 == z24 : Bool}
  for e25: {y25 == z25 : Bool}
  for e26: {y26 == z26 : Bool}
  for e27: {y27 == z27 : Bool}
  for e28: {y28 == z28 : Bool}
  for e29: {y29 == z29 : Bool}
  for e30: {y30 == z30 : Bool}
  for e31: {y31 == z31 : Bool}
  {U32{WCon{y0, WCon{y1, WCon{y2, WCon{y3, WCon{y4, WCon{y5, WCon{y6, WCon{y7, WCon{y8, WCon{y9, WCon{y10, WCon{y11, WCon{y12, WCon{y13, WCon{y14, WCon{y15, WCon{y16, WCon{y17, WCon{y18, WCon{y19, WCon{y20, WCon{y21, WCon{y22, WCon{y23, WCon{y24, WCon{y25, WCon{y26, WCon{y27, WCon{y28, WCon{y29, WCon{y30, WCon{y31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} == U32{WCon{z0, WCon{z1, WCon{z2, WCon{z3, WCon{z4, WCon{z5, WCon{z6, WCon{z7, WCon{z8, WCon{z9, WCon{z10, WCon{z11, WCon{z12, WCon{z13, WCon{z14, WCon{z15, WCon{z16, WCon{z17, WCon{z18, WCon{z19, WCon{z20, WCon{z21, WCon{z22, WCon{z23, WCon{z24, WCon{z25, WCon{z26, WCon{z27, WCon{z28, WCon{z29, WCon{z30, WCon{z31, WNil{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}} : U32}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil