proposition: Lemma putpermsC (x : S) A (s : seq A) B (f : _ -> M B) : put x >> (perms s >>= f) = perms s >>= (fun rs => put x >> f rs).
proof: Proof. move Hn : (size s) => n. elim: n s Hn x f => [|n IH] s Hn x f. by case: s Hn => // _; rewrite permsE 2!bindretf. case: s Hn => // h t [Hn]. rewrite tpermsE 2!bindA puttselectC; bind_ext; case=> a b. rewrite 2!bindA. have bn : size b = n by rewrite size_tuple. rewrite IH //. under eq_bind do rewrite bindretf. by under [RHS]eq_bind do rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib