proposition: Remark denote_p_nonce_twice : denote _ bool p_nonce_twice = nonce_twice.
proof: Proof. by []. Qed.
imports: Eqdep JMeq List ssreflect mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) hierarchy monad_lib state_lib trace_lib monad_model