law length_append

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/chacha/involution.bend:46

import Base

46law length_append:
47  for +xs: List<&2, U32>
48  for +ys: List<&2, U32>
49  {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}