Bytes.len_rev: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
Lines 96-105 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&start_line=96&end_line=105

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

def len_rev(xs: List<&2, U32>) -> {List.length(&2, U32, List.reverse(&2, U32, xs)) == List.length(&2, U32, xs) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +t:
      %Equal.sym(List<&2, U32>, List.reverse(&2, U32, x <> t), List.append(&2, U32, List.reverse(&2, U32, t), [x]), rev_cons(x, t)) : {List.length(&2, U32, _) == 1n+List.length(&2, U32, t) : Nat}
      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, List.reverse(&2, U32, t), [x])), Nat.add(List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, [x])), len_app(List.reverse(&2, U32, t), [x])) : {_ == 1n+List.length(&2, U32, t) : Nat}
      %Equal.sym(Nat, List.length(&2, U32, List.reverse(&2, U32, t)), List.length(&2, U32, t), len_rev(t)) : {Nat.add(_, List.length(&2, U32, [x])) == 1n+List.length(&2, U32, t) : Nat}
      %Equal.sym(Nat, 1n+List.length(&2, U32, t), Nat.add(List.length(&2, U32, t), 1n), SR.succ_add(1n, List.length(&2, U32, t))) : {Nat.add(List.length(&2, U32, t), 1n) == _ : Nat}
      {==}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=len_app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=rev_cons
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=succ_add