law add_length

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/hash/lists.bend:81

import Base

81# n + |xs| + |ys| == n + |xs ++ ys|
82law add_length:
83  for +n: Nat
84  for +xs: List<&2, U32>
85  for +ys: List<&2, U32>
86  {Nat.add(Nat.add(n, List.length(&2, U32, xs)), List.length(&2, U32, ys)) == Nat.add(n, List.length(&2, U32, List.append(&2, U32, xs, ys))) : Nat}