proposition: Lemma st_get_get (M : stateReifyMonad S) s : reify (st_get : MN _) s = assoc_opt (reify (get : M _) s.1, s.2).
proof: Proof. by case: s => s1 s2; rewrite reifyget reifystget. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) ihierarchy imonad_lib