proposition: Lemma If_Then_Else_Bind {sz} {C ResultT : Type} : forall (w w' : word sz) (b : B) (cd : CacheDecode) (dec_c : B -> CacheDecode -> option (C * B * CacheDecode)) (k : C -> B -> CacheDecode -> option (ResultT * B * CacheDecode)), (if weq w w' then `(c, b', cd') <- dec_c b cd; k c b' cd' else None) = (`(c, b', cd') <- dec_c b cd; if weq w w' then k c b' cd' else None).
proof: Proof. intros; find_if_inside; eauto. destruct (dec_c b cd) as [ [ [? ?] ? ] | ]; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word