def rows8_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/hash.bend:249
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
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
249def rows8_eq(+ws: List<&2, U32>) -> {SB.rows8(ws) == SA.rows_of0(SA.row_of(ws)) : A.Block}:
250 Equal.trans(A.Block, SB.rows8_0(SB.row(ws)), SB.rows8_0(SA.row_of(ws)), SA.rows_of0(SA.row_of(ws)),
251 Equal.cong(T.State & List<&2, U32>, A.Block, z => SB.rows8_0(z), SB.row(ws), SA.row_of(ws), row_eq(ws)),
252 rows_eq0(SA.row_of(ws)))