proposition: Remark denote_countdown fuel : denote ([the stateTraceMonad nat bool of (StateMonad.acto (nat * seq bool)%type)]) unit (p_countdown fuel) = countdown fuel.
proof: Proof. elim: fuel => // n. rewrite [countdown (S n)]/=. by move <-. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model