def tr.join_eq

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

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

1013def tr.join_eq(+bs: List<&2, M.CmBlock>, +rest: List<&2, U32>) -> {M.cm.join_onto(bs, rest) == M.cm.join_onto.fast(bs, rest) : List<&2, U32>}:
1014  Equal.sym(List<&2, U32>, M.cm.join_onto.fast(bs, rest), M.cm.join_onto(bs, rest), tr.join_go(bs, Nil{}, rest))