XOR by a fixed mask is self-inverse on `BitVec`: `c = k ^^^ m ↔ c ^^^ m = k`. -/ https://github.com/leanprover/cslib/blob/906574d376632467fd84a2a404efbe58a95fc13c/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean#L27-L28
XOR by a fixed mask is self-inverse on
BitVec:c = k ^^^ m ↔ c ^^^ m = k. -/cslib/Cslib/Crypto/Protocols/PerfectSecrecy/Internal/OneTimePad.lean
Lines 27 to 28 in 906574d