def stb256_len_list
bend-osdev-hashes@0.1.0.0 · PROOF.bend:109
import bend-osdev-hashes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
109def stb256_len_list(a8: U32, a9: U32, a10: U32, a11: U32, a12: U32, a13: U32, a14: U32, a15: U32) -> {B.len(B.append(B.le32(a8), B.append(B.le32(a9), B.append(B.le32(a10), B.append(B.le32(a11), B.append(B.le32(a12), B.append(B.le32(a13), B.append(B.le32(a14), B.le32(a15))))))))) == 32n : Nat}:
110 match a8 a9 a10 a11 a12 a13 a14 a15:
111 case U32{wa8} U32{wa9} U32{wa10} U32{wa11} U32{wa12} U32{wa13} U32{wa14} U32{wa15}:
112 {==}