fact: Definition Enqueue_Decode : DecodeM (S * T) T := fun t env => Ifopt dequeue_opt t as st Then Some (st, env) Else None.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs