proposition: Lemma lemma32 a : foldl op b (o) insert a = Ret \o foldl op b \o (rcons^~ a) :> (_ -> M _).
proof: Proof. rewrite boolp.funeqE; elim/last_ind => [/=|xs y IH]. by rewrite fcompE insertE fmapE bindretf. rewrite fcompE. rewrite insert_rcons. rewrite alt_fmapDr fmapE bindretf. rewrite -fmap_oE. have H : forall w, foldl op b \o rcons^~ w = op^~ w \o foldl op b. by move=> w; rewrite boolp.funeqE => ws /=; rewrite -cats1 foldl_cat. rewrite (H y). rewrite fmap_oE. rewrite fcompE in IH. rewrite IH. rewrite -[in X in _ [~] X]bindretf. rewrite bindretf. rewrite -{1}compA. rewrite fmapE bindretf. rewrite (H a). rewrite [in X in _ [~] X]/=. rewrite opP. rewrite /= -!cats1 -catA /=. rewrite foldl_cat /=. by rewrite altmm. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib