proposition: Lemma st_put_put (M : stateReifyMonad S) s s' : reify (st_put s' : MN _) s = assoc_opt (reify (put s' : M _) s.1, s.2).
proof: Proof. by case: s => s1 s2; rewrite reifyput reifystput. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) ihierarchy imonad_lib