def des_swap2

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:166

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/des.bend as D

166def des_swap2(h: D.LcDesHalves) -> {h == D.des.swap(D.des.swap(h)) : D.LcDesHalves}:
167  match h:
168    case D.LcDesHalves{l, r}:
169      {==}