proposition: Lemma DecodeBindOpt2_under_bind {S T V D E} : forall (a_opt : option (S * T * D)) (f f' : S -> T -> D -> option (V * E * D)), (forall a b d, f a b d = f' a b d) -> DecodeBindOpt2 a_opt f = DecodeBindOpt2 a_opt f'.
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