Hash.rows_eq0: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
Lines 242-247 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&start_line=242&end_line=247

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend as SB
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

def rows_eq0(p: T.State & List<&2, U32>) -> {SB.rows8_0(p) == SA.rows_of0(p) : A.Block}:
  match p:
    case Tuple{+x, +ws}:
      Equal.trans(A.Block, SB.rows8_1(x, SB.row(ws)), SB.rows8_1(x, SA.row_of(ws)), SA.rows_of1(x, SA.row_of(ws)),
        Equal.cong(T.State & List<&2, U32>, A.Block, z => SB.rows8_1(x, z), SB.row(ws), SA.row_of(ws), row_eq(ws)),
        rows_eq1(x, SA.row_of(ws)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  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/proofs/crypto/argon2/hash.bend&name=row_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&name=rows_eq1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=row_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=rows_of0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=rows_of1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=row
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=State