fact: Definition foreach (M : monad) (items : list nat) (body : nat -> contT unit M unit) : M unit := foldr (fun x next => (body x) (fun _ => next)) (Ret tt) items.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib