fact: Fixpoint encode_word' (s : nat) (w : word s) (b' : T) : T := match w with | WO => b' | WS b s' w' => enqueue_opt b (encode_word' s' w' b') end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats