XOR by a fixed mask is self-inverse on `BitVec`: `c = k ^^^ m ↔ c ^^^ m = k`. -/ https://github.com/crei/cslib/blob/c1f2e8ee0d9ac0a955793f665a656958e924779f/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 c1f2e8e