proposition: Lemma theorem46lid z zs : z = foldl mul b zs -> aggregate b mul add = Ret \o foldl mul b \o flatten :> (_ -> M _) -> z = add b z.
proof: Proof. move=> zzs H. transitivity (foldl mul b (flatten [:: zs])). by rewrite /= cats0. transitivity (foldl add b (map (foldl mul b) [:: zs])). have Hm : iperm [:: zs] = Ret [:: zs] [~] fail :> M _. by rewrite /= bindretf insertE altmfail. by rewrite (lemma45a idempotent_converse injective_return H). by rewrite /= -zzs. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib