fact: Definition does_swap (m : M unit) := (do x <- aget false ; do y <- aget true ; m >> do x' <- aget false ; do y' <- aget true ; Ret ((x == y') && (y == x'))).
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib