proposition: Lemma DecodeOpt2_fmap_if {S S' P P'} : forall (f : S -> S') (b : {P} + {P'}) (a_opt a_opt' : option S), DecodeOpt2_fmap f (if b then a_opt else a_opt') = if b then (DecodeOpt2_fmap f a_opt) else (DecodeOpt2_fmap f a_opt').
proof: Proof. intros; find_if_inside; reflexivity. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache