law prefix_suffix

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/sound.bend:40

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as RC

40law prefix_suffix:
41  for +n: Nat
42  for +xs: List<&2, U32>
43  {List.append(&2, U32, RC.prefix(n, xs), RC.suffix(n, xs)) == xs : List<&2, U32>}