proposition: Lemma optimize_if_bind2_bool {A A' B C} : forall (c : bool) (t e : option (A * B * C)) (k : A -> B -> C -> option (A' * B * C)), (`(a, b, env) <- (if c then t else e); k a b env) = if c then `(a, b, env) <- t; k a b env else `(a, b, env) <- e; k a b env.
proof: Proof. destruct c; congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Bool.Bool Coq.ZArith.ZArith Fiat.Common.DecideableEnsembles Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.Tactics.CacheStringConstant Fiat.Common.IterateBoundedIndex Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.Empty Fiat.Narcissus.Formats.Option Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Common.Sig Fiat.Narcissus.Automation.Common Fiat.Narcissus.Automation.NormalizeFormats Fiat.Narcissus.Automation.Decision Fiat.Narcissus.Automation.ExtractData Fiat.Narcissus.Automation.SynthesizeDecoder