def okb_con
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/bytes.bend:114
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytes
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
114def okb_con(+n: Nat, +x: U32, +t: List<&2, U32>, +hx: {Nat.is_le(v(x), 255n) == True{} : Bool}, +ht: {LM.okb(n, t, 255n) == True{} : Bool}) -> {LM.okb(1n+n, Con{x, t}, 255n) == True{} : Bool}:
115 L.and_intro(Nat.is_le(v(x), 255n), LM.okb(n, t, 255n), hx, ht)