proposition: Lemma safeE : safe =1 safeAcc 0 [::] [::].
proof: Proof. move=> s; rewrite /safe /safeAcc. by rewrite (sub_all _ (@all_predT _ _)) // (sub_all _ (@all_predT _ _)) // !andbT. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib