fact: Definition StrictTerminal_Decode (s : S) : DecodeM S T := fun t env => If (beq_nat (bin_measure t) 0) Then Some (s, env) Else None.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs