proposition: Lemma deter_aggregate : deterministic (aggregate b mul add : _ -> M _).
proof: Proof. rewrite /deterministic aggregateE //; eexists; reflexivity. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib