def pfst
import bend-collections-laws-math@1.0.0.0/proofs/math/random/below.bend as Belowimport Base
64def pfst(-S: Data, p: Nat & S) -> Nat:
65 (k, s) = p
66 k
import bend-collections-laws-math@1.0.0.0/proofs/math/random/below.bend as Belowimport Base
64def pfst(-S: Data, p: Nat & S) -> Nat:
65 (k, s) = p
66 k