def app_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/random/bytes.bend:21

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

21def app_nil(+xs: List<&2, U32>) -> {SCR.append(xs, []) == xs : List<&2, U32>}:
22  match xs:
23    case Nil{}:
24      {==}
25    case Con{+x, +rest}:
26      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{x, l}, SCR.append(rest, []), rest, app_nil(rest))