fact: Definition Compose_Encode {S' : Type} (encode : EncodeM S' T) (f' : S -> option S') : EncodeM S T := fun s => Ifopt f' s as s' Then encode s' Else fun _ => None.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs