fact: Definition DecodeOpt2_fmap_compose {S S' S''} : forall (f : S -> S') (f' : S' -> S'') (a_opt : option S), DecodeOpt2_fmap f' (DecodeOpt2_fmap f a_opt) = DecodeOpt2_fmap (compose f' f) a_opt.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache