Point.allred_app: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as Point
Lines 106-111 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&start_line=106&end_line=111

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

def allred_app(+one: Nat, rs: List<&2, List<&2, Nat>>, +x: List<&2, Nat>, +h: {allred(one, rs) == True{} : Bool}, +hx: {red(one, x) == True{} : Bool}) -> {allred(one, List.append(&2, List<&2, Nat>, rs, [x])) == True{} : Bool}:
  match rs:
    case Nil{}:
      Lg.and_intro(red(one, x), True{}, hx, {==})
    case +r <> +t:
      Lg.and_intro(red(one, r), allred(one, List.append(&2, List<&2, Nat>, t, [x])), Lg.and_left(red(one, r), allred(one, t), h), allred_app(one, t, x, Lg.and_right(red(one, r), allred(one, t), h), hx))

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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=allred
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend&name=red
  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