def le_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:77

import Base

77def le_len(+xs: List<&2, U32>, +k: Nat, +e: {List.length(&2, U32, xs) == 32n : Nat}, +h: {Nat.is_le(k, 32n) == True{} : Bool}) -> {Nat.is_le(k, List.length(&2, U32, xs)) == True{} : Bool}:
78  %Equal.sym(Nat, List.length(&2, U32, xs), 32n, e) : {Nat.is_le(k, _) == True{} : Bool}
79  h