proposition: Lemma hyloME y : hyloM y = if p y then Ret e else f y >>= (fun xz => op xz.1 (hyloM xz.2)).
proof: Proof. rewrite /hyloM Init.Wf.Fix_eq; last first. move => b g g' K; rewrite /hyloM'; case: ifPn => // pb. bind_ext => -[a' b'] /=. destruct Bool.bool_dec => //. by rewrite K. rewrite {1}/hyloM'; case: ifPn => // py. rewrite Hdecr_seed /bassert !bindA. bind_ext => -[b' a']. case: assertPn => Hseed; last by rewrite 2!bindfailf. by rewrite 2!bindretf Hseed. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)