proposition: Lemma reify_safe2 crs updowns : reify (safe2 crs : M _) updowns = Some (safe1 updowns crs).
proof: Proof. rewrite safe2E reifybind reifyget; case: safe1 => a b. by rewrite reifybind reifyput reifyret. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib