proposition: Lemma If_sumbool_Then_Else_DecodeBindOpt {S T T' ResultT ResultT'} {c : Cache} {P} : forall (a_eq_dec : forall a a' : S, {P a a'} + {~ P a a'}) a a' (k : _ -> _ -> _ -> option (ResultT' * T' * CacheDecode)) (t : P a a' -> option (ResultT * T * CacheDecode)) (e : ~ P a a' -> option (ResultT * T * CacheDecode)), (`(w, b', cd') <- match a_eq_dec a a' with | left e => t e | right n => e n end; k w b' cd') = match a_eq_dec a a' with | left e => `(w, b', cd') <- t e; k w b' cd' | right n => `(w, b', cd') <- e n; k w b' cd' end.
proof: Proof. intros; destruct (a_eq_dec a a'); simpl; intros; reflexivity. 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