def c6_unop_op
import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend as C6
1683def c6_unop_op(o: C6.LcCast6Op, +s: M.CmBlock) -> {s == C6.c6.unop(o, C6.c6.op(o, s)) : M.CmBlock}:
1684 match o:
1685 case C6.LcCast6Op{fwd, +k}:
1686 match fwd:
1687 case True{}:
1688 c6_qq(k, s)
1689 case False{}:
1690 c6_qbq(k, s)