def swap2

bend-osdev-cast5@0.1.0.0 · PROOF.bend:9

import Base
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L

9def swap2(b: L.LcBlock64) -> {b == L.lc.swap(L.lc.swap(b)) : L.LcBlock64}:
10  match b:
11    case L.LcBlock64{h, l}:
12      {==}