def cat2_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/top.bend:81

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as BY

81def cat2_eq(+x: List<&2, U32>, +sx: List<&2, U32>, +y: List<&2, U32>, +sy: List<&2, U32>, +m: List<&2, U32>, +ex: {x == sx : List<&2, U32>}, +ey: {y == sy : List<&2, U32>}) -> {E.cat(x, E.cat(y, m)) == SE.cat(sx, SE.cat(sy, m)) : List<&2, U32>}:
82  +e1 = BY.cat_eq(x, E.cat(y, m))
83  +e2 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(x, z), E.cat(y, m), SE.cat(y, m), BY.cat_eq(y, m))
84  +e3 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(z, SE.cat(y, m)), x, sx, ex)
85  +e4 = Equal.cong(List<&2, U32>, List<&2, U32>, z => SE.cat(sx, SE.cat(z, m)), y, sy, ey)
86  Equal.trans(List<&2, U32>, E.cat(x, E.cat(y, m)), SE.cat(x, E.cat(y, m)), SE.cat(sx, SE.cat(sy, m)), e1, Equal.trans(List<&2, U32>, SE.cat(x, E.cat(y, m)), SE.cat(x, SE.cat(y, m)), SE.cat(sx, SE.cat(sy, m)), e2, Equal.trans(List<&2, U32>, SE.cat(x, SE.cat(y, m)), SE.cat(sx, SE.cat(y, m)), SE.cat(sx, SE.cat(sy, m)), e3, e4)))