proposition: Lemma aswapxx i : aswap i i = skip.
proof: Proof. rewrite /aswap agetget. under eq_bind do rewrite aputput. by rewrite agetputskip. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib