First let's do the proof for the classical case:

------------------

Def: torev f = \ (a,b) -> (a, xor (f a) b)

Claim: \ (a,b) -> torev f (torev f (a,b)) = id
Proof:

  \ (a,b) -> torev f (a, xor (f a) b) 
= \ (a,b) -> (a, xor (f a) (xor (f a) b))
= \ (a,b) -> (a, xor b (xor (f a) (f a)))
= \ (a,b) -> (a, xor b False)
= \ (a,b) -> (a, b)
= id

------------------

Let's try to generalize to the quantum case:

Def: torev f = \ (a,b) -> f a @>>= \ b' -> vreturn (a, xor b b')

Claim: \ (a0,b0) -> torev f (a0,b0) @>>= \ (a1,b1) -> 
                    torev f (a1,b1) 
     = \ (a0,b0) -> vreturn (a0,b0)
Proof:
  \ (a0,b0) -> torev f (a0,b0) @>>= \ (a1,b1) -> 
               torev f (a1,b1) 
= \ (a0,b0) -> f a0 @>>= \ b' -> 
               vreturn (a0, xor b0 b') @>>= \ (a1,b1) -> 
               f a1 @>>= \ b'' -> 
               vreturn (a1, xor b1 b'')
= \ (a0,b0) -> f a0 @>>= \ b' -> 
               f a0 @>>= \ b'' -> 
               vreturn (a0, xor (xor b0 b') b'')

Assume that two applications of f to the same value return the
same result.  This is not true in some monads. It would need
to be proved for the two monads we consider: Classical and Quantum. 

= \ (a0,b0) -> f a0 @>>= \ b' -> 
               vreturn (a0, xor (xor b0 b') b')
= \ (a0,b0) -> f a0 @>>= \ b' -> 
               vreturn (a0, xor b0 (xor b' b'))
= \ (a0,b0) -> f a0 @>>= \ b' -> 
               vreturn (a0, b0)
= \ (a0,b0) -> f a0 @>>= \ _ -> 
               vreturn (a0, b0)

Assume that it is ok to throw away the result of applying a
function. This is not true in some monads. It would need to be
proved for the two monads we consider: Classical and Quantum.

= \ (a0,b0) -> vreturn (a0, b0)