proposition: Lemma If_Opt_Then_Else_BindOpt {S T V} : forall (a_opt : option S) (t : S -> option T) (e : option T) (k : _ -> option V), BindOpt (Ifopt a_opt as a Then t a Else e) k = Ifopt a_opt as a Then (BindOpt (t a) k) Else (BindOpt e k).
proof: Proof. destruct a_opt; simpl; intros; 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