def app_assoc

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

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

28def app_assoc(+xs: List<&2, U32>, +ys: List<&2, U32>, +zs: List<&2, U32>) -> {SCR.append(SCR.append(xs, ys), zs) == SCR.append(xs, SCR.append(ys, zs)) : List<&2, U32>}:
29  match xs:
30    case Nil{}:
31      {==}
32    case Con{+x, +rest}:
33      Equal.cong(List<&2, U32>, List<&2, U32>, l => Con{x, l}, SCR.append(SCR.append(rest, ys), zs), SCR.append(rest, SCR.append(ys, zs)), app_assoc(rest, ys, zs))