def tr.split_fin_nil

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

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

929def tr.split_fin_nil(+s: M.CmSplit) -> {tr.split_fin(Nil{}, s) == s : M.CmSplit}:
930  match s:
931    case M.CmSplit{bs, t}:
932      {==}