proposition: Lemma DecodeBindOpt_inv {V} (a_opt : option (S * T)) (a : V * T) (k : S -> T -> option (V * T)) : DecodeBindOpt a_opt k = Some a -> exists a' b', a_opt = Some (a', b') /\ Some a = k a' b'.
proof: Proof. unfold DecodeBindOpt; destruct a_opt as [ [a' b'] | ]; 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