def swap2

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

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L

1449def swap2(b: L.LcBlock64) -> {b == L.lc.swap(L.lc.swap(b)) : L.LcBlock64}:
1450  match b:
1451    case L.LcBlock64{h, l}:
1452      {==}