proposition: Lemma DecodeBindOpt2_assoc {S T V D E F G} : forall (a_opt : option (S * T * D)) (f : S -> T -> D -> option (V * E * D)) (g : V -> E -> D -> option (F * G * D)), DecodeBindOpt2 (DecodeBindOpt2 a_opt f) g = DecodeBindOpt2 a_opt (fun a b c => DecodeBindOpt2 (f a b c) 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