PROOF.tr.split_fin: def of bend-osdev-cipher-modes@0.1.0.0
Import: import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
Lines 919-922 of bend-osdev-cipher-modes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-cipher-modes@0.1.0.0/PROOF.bend&start_line=919&end_line=922

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

def tr.split_fin(acc: List<&2, M.CmBlock>, s: M.CmSplit) -> M.CmSplit:
  match s:
    case M.CmSplit{bs, t}:
      M.CmSplit{M.cm.blocks.rev_onto(acc, bs), t}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmSplit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=cm.blocks.rev_onto