def fh8
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:250
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
250def fh8(+x: Nat, +f16: {C.fits(16n, x) == True{} : Bool}) -> {C.fits(8n, C.high(8n, x)) == True{} : Bool}:
251 %Equal.sym(Nat, C.high(8n, C.high(8n, x)), C.high(16n, x), Equal.sym(Nat, C.high(16n, x), C.high(8n, C.high(8n, x)), WW.high_comp(8n, 8n, x))) : {Nat.is_eq(_, 0n) == True{} : Bool}
252 f16