proposition: Lemma iperm_idempotent (E : eqType) : iperm >=> iperm = iperm :> (seq E -> M _).
proof: Proof. apply: funext_dep => s; rewrite kleisliE. elim: s => [|h t ih]; first by rewrite /= bindretf. rewrite /= -[in RHS]ih !bindA; bind_ext. elim/last_ind => [|s x _]. by rewrite insertE /= !bindretf insertE /= bindretf insertE. rewrite iperm_insertC insert_rcons alt_bindDl bind_fmap /= /comp /=. under [in RHS]eq_bind do rewrite iperm_rcons_bind. rewrite bindretf (@perm_eq_iperm _ _ (h :: rcons s x)); last first. by rewrite -cats1 -cat1s catA perm_catC. rewrite /= iperm_insertC -alt_bindDr; bind_ext => s'. by rewrite altmm iperm_rcons_bind. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)