proposition: Lemma BindOpt_assoc {S''' S' S''} : forall (a_opt : option S''') (f : S''' -> option S') (g : S' -> option S''), BindOpt (BindOpt a_opt f) g = BindOpt a_opt (fun a => BindOpt (f a) g).
proof: Proof. destruct a_opt as [ ? | ]; simpl; intros; eauto. 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