def sp.cons_blocks

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:124

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

124def sp.cons_blocks(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.blocks(M.cm.split.cons(b, s)) == Con{b, M.cm.split.blocks(s)} : List<&2, M.CmBlock>}:
125  match s:
126    case M.CmSplit{bs, t}:
127      {==}