def tr.split_eq
bend-osdev-mode-core@0.1.0.0 · PROOF.bend:601
import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
601def tr.split_eq(+xs: List<&2, U32>) -> {M.cm.split(xs) == M.cm.split.fast(xs) : M.CmSplit}:
602 Equal.sym(M.CmSplit, M.cm.split.fast(xs), M.cm.split(xs), Equal.trans(M.CmSplit, M.cm.split.go(xs, Nil{}), tr.split_fin(Nil{}, M.cm.split(xs)), M.cm.split(xs), tr.split_go(xs, Nil{}), tr.split_fin_nil(M.cm.split(xs))))