def length_drop

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

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

47def length_drop(+xs: List<&2, U32>, +n: Nat) -> {SC.length(U32, SC.drop(U32, xs, n)) == Nat.sub(SC.length(U32, xs), n) : Nat}:
48  match xs n:
49    case Nil{} _:
50      Equal.sym(Nat, Nat.sub(0n, n), 0n, zsub(n))
51    case Con{h, t} 0n:
52      {==}
53    case Con{+h, +t} 1n+ +p:
54      length_drop(t, p)