def skip_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:321

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li

321def skip_succ(+k: Nat, +ds: List<&2, U32>) -> {Li.skip(1n+k, ds) == Li.skip(k, Li.tl(ds)) : List<&2, U32>}:
322  match ds:
323    case Nil{}: Equal.sym(List<&2, U32>, Li.skip(k, []), [], skip_nil(k))
324    case x <> t: {==}