def take_drop

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:31

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

31def take_drop(+xs: List<&2, U32>, +n: Nat) -> {SC.append(U32, SC.take(U32, xs, n), SC.drop(U32, xs, n)) == xs : List<&2, U32>}:
32  match xs n:
33    case Nil{} _:
34      {==}
35    case Con{h, t} 0n:
36      {==}
37    case Con{+h, +t} 1n+ +p:
38      Equal.cong(List<&2, U32>, List<&2, U32>, z => Con{h, z}, SC.append(U32, SC.take(U32, t, p), SC.drop(U32, t, p)), t, take_drop(t, p))