def length_append

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:69

import Base

69def length_append(+xs: List<&2, U32>, +ys: List<&2, U32>) -> {List.length(&2, U32, List.append(&2, U32, xs, ys)) == Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}:
70  match xs:
71    case Nil{}:
72      {==}
73    case +x <> +rest:
74      %length_append(rest, ys) : {1n+List.length(&2, U32, List.append(&2, U32, rest, ys)) == 1n+_ : Nat}
75      {==}