proposition: Lemma rev_insert : rev (o) insert a = insert a \o rev :> (_ -> M _).
proof: Proof. apply boolp.funext; elim => [|h t ih]. by rewrite fcompE insertE fmapE bindretf. rewrite fcompE insertE compE alt_fmapDr fmapE bindretf compE [in RHS]rev_cons. rewrite insert_rcons rev_cons -cats1 rev_cons -cats1 -catA; congr (_ [~] _). move: ih; rewrite fcompE [X in X -> _]/= => <-. rewrite -!fmap_oE. congr (fmap _ (insert a t)). by apply boolp.funext => s; rewrite /= -rev_cons. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)