proposition: Lemma getpermsC A (s : seq A) B (f : _ -> _ -> M B) : (get >>= (fun ini => perms s >>= f^~ ini) = perms s >>= (fun rs => get >>= f rs))%Do.
proof: Proof. move Hn : (size s) => n. elim: n s Hn f => [|n IH] s Hn f. case: s Hn => // _; rewrite permsE. by rewrite bindretf; under eq_bind do rewrite bindretf. case: s Hn => // h t [Hn]. rewrite tpermsE bindA. transitivity (do x <- tselect (h :: t); do ini <- get; do rs <- perms x.2; f (x.1 :: rs) ini)%Do; last first. bind_ext => x. rewrite IH ?size_tuple // bindA. by under [RHS]eq_bind do rewrite bindretf. rewrite -gettselectC. bind_ext => x. rewrite bindA; bind_ext => rs. rewrite bindA. by under eq_bind do rewrite bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib