fact: Definition option_encode (encode_Some : EncodeM S T) (encode_None : EncodeM () T) : EncodeM (option S) T := fun a_opt => If_Opt_Then_Else a_opt encode_Some (encode_None ()).
imports: Fiat.Common Fiat.Computation Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats