proposition: Lemma optimize_under_DecodeBindOpt2_both {S T V D E} {T' } : forall (a_opt : option (S * T * V)) (a_opt' : option (S * T' * V)) (g : T' -> T) (a_opt_eq_Some : forall a' b' c, a_opt' = Some (a', b', c) -> a_opt = Some (a', g b', c)) (a_opt_eq_None : a_opt' = None -> a_opt = None) (k : _ -> _ -> _ -> option (D * E * V)) (k' : _ -> _ -> _ -> _) (k_eq_Some : forall a' b' c, a_opt' = Some (a', b', c) -> k a' (g b') c = k' a' b' c), DecodeBindOpt2 a_opt k = DecodeBindOpt2 a_opt' k'.
proof: Proof. destruct a_opt' as [ [ [? ?] ?] | ]; simpl; intros. erewrite a_opt_eq_Some; simpl; eauto. erewrite a_opt_eq_None; simpl; 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