proposition: Lemma iperm_rcons_bind (E : eqType) (s : seq E) x : iperm (rcons s x) = iperm s >>= (fun s' => iperm (rcons s' x)) :> M _.
proof: Proof. have [n ns] := ubnP (size s); elim: n s ns x => // n ih. case=> [_ x|h t]; first by rewrite /= 2!bindretf /= bindretf. rewrite ltnS /= => tn x; rewrite ih// !bindA. by under [in RHS]eq_bind do rewrite -iperm_insertC. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)