Bitsv.all01_app: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as Bitsv
Lines 37-42 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend&start_line=37&end_line=42

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

def all01_app(xs: List<&2, Nat>, +ys: List<&2, Nat>, +hx: {all01(xs) == True{} : Bool}, +hy: {all01(ys) == True{} : Bool}) -> {all01(List.append(&2, Nat, xs, ys)) == True{} : Bool}:
  match xs:
    case Nil{}:
      hy
    case +x <> +t:
      Lg.and_intro(Nat.is_lt(x, 2n), all01(List.append(&2, Nat, t, ys)), Lg.and_left(Nat.is_lt(x, 2n), all01(t), hx), all01_app(t, ys, Lg.and_right(Nat.is_lt(x, 2n), all01(t), hx), hy))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend&name=all01
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_intro
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right