proposition: Lemma DecodeBindOpt2_inv {V D E} (a_opt : option (S * T * D)) (a : V * E * D) (k : S -> T -> D -> option (V * E * D)) : DecodeBindOpt2 a_opt k = Some a -> exists a' b' d', a_opt = Some (a', b', d') /\ Some a = k a' b' d'.
proof: Proof. unfold DecodeBindOpt2; destruct a_opt as [ [ [a' b'] d'] | ]; simpl; intros; first [discriminate | injections ]. eexists _, _, _; intuition 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