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