Cipher.quad_cong: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as Cipher
Lines 13-27 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend&start_line=13&end_line=27

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as T

# Congruence of the record constructors (one rewrite per field, on variables).
law quad_cong:
  for +a: U32
  for +b: U32
  for +c: U32
  for +d: U32
  for +a2: U32
  for +b2: U32
  for +c2: U32
  for +d2: U32
  for +ea: {a == a2 : U32}
  for +eb: {b == b2 : U32}
  for +ec: {c == c2 : U32}
  for +ed: {d == d2 : U32}
  {T.W{a, b, c, d} == T.W{a2, b2, c2, d2} : T.Quad}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend&name=Quad