def prefix_first

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/blist.bend:38

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B

38def prefix_first(n: Nat, bs: List<&2, U32>) -> {B.prefix(n, bs) == CV.first(n, bs) : List<&2, U32>}:
39  match n bs:
40    case 0n _:
41      {==}
42    case 1n+k Nil{}:
43      {==}
44    case 1n+ +k +b <> t:
45      Equal.cong(List<&2, U32>, List<&2, U32>, l => b <> l, B.prefix(k, t), CV.first(k, t), prefix_first(k, t))