proposition: Lemma foldt_universal : h = foldt f g.
proof: Proof. rewrite boolp.funeqE; elim => [a|]; first by rewrite -H1. by move=> t1 IH1 t2 IH2 /=; rewrite -IH1 -IH2 -(uncurryE Bin) -compE H2. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib