def keep_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/fill.bend:309

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A

309def keep_len(+m1: List<&2, A.Block>, +m2: List<&2, A.Block>, +x: Nat, +e: {SC.length(A.Block, m2) == SC.length(A.Block, m1) : Nat}, +h: {SC.length(A.Block, m1) == x : Nat}) -> {SC.length(A.Block, m2) == x : Nat}:
310  Equal.trans(Nat, SC.length(A.Block, m2), SC.length(A.Block, m1), x, e, h)