def len_app

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:89

import Base

89def len_app(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}:
90  match xs:
91    case Nil{}:
92      {==}
93    case +x <> +t:
94      Equal.cong(Nat, Nat, n => 1n+n, List.length(&2, U32, List.append(&2, U32, t, ys)), Nat.add(List.length(&2, U32, t), List.length(&2, U32, ys)), len_app(t, ys))