def sp.cons_tail

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:85

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

85def sp.cons_tail(b: M.CmBlock, s: M.CmSplit) -> {M.cm.split.tail(M.cm.split.cons(b, s)) == M.cm.split.tail(s) : List<&2, U32>}:
86  match s:
87    case M.CmSplit{bs, t}:
88      {==}