fact: Fixpoint foldt B (f : A -> B) (g : B * B -> B) (t : Tree) : B := match t with | Tip a => f a | Bin t u => g (foldt f g t, foldt f g u) end.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib