proposition: Lemma BindOpt_map_if {S S' P P'} : forall (f : option S -> S') (b : {P} + {P'}) (a_opt a_opt' : option S), f (if b then a_opt else a_opt') = if b then (f a_opt) else (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