proposition: Lemma writeList_aswap i x h (t : seq E) : writeList i (rcons (h :: t) x) = writeList i (rcons (x :: t) h) >> aswap i (i + size (rcons t h)).
proof: Proof. rewrite /aswap -!bindA writeList_rcons /=. rewrite aput_writeListC// bindA aput_writeListC// writeList_rcons !bindA. bind_ext => -[]. under [RHS] eq_bind do rewrite -bindA. rewrite aputget -bindA size_rcons addSnnS. under [RHS] eq_bind do rewrite -!bindA. rewrite aputgetC; last by rewrite -addSnnS ltn_eqF// ltn_addr. rewrite -!bindA aputget aputput aputC; last by right. by rewrite bindA aputput. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib