Peth.sw_is: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/peth.bend as Peth
Lines 74-79 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/peth.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/peth.bend&start_line=74&end_line=79

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES

def sw_is(+h: ES.Hash, pk: List<&2, U32>) -> {ES.eth_with(h, pk) == ES.eth_go(h, pk) : Maybe<&2, List<&2, U32>>}:
  match pk:
    case Nil{}:
      {==}
    case b <> t:
      {==}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=Hash
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=eth_go
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=eth_with