proposition: Lemma If_Opt_Then_Else_DecodeBindOpt_swap {A C ResultT : Type} : forall (a_opt : option A) (b : B) (cd : CacheDecode) (dec_c : B -> CacheDecode -> option (C * B * CacheDecode)) (k : A -> C -> B -> CacheDecode -> option (ResultT * B * CacheDecode)), (`(a, b', cd') <- Ifopt a_opt as a Then Some (a, b, cd) Else None; `(c, b', cd') <- dec_c b' cd'; k a c b' cd') = (`(c, b', cd') <- dec_c b cd; `(a, b', cd') <- Ifopt a_opt as a Then Some (a, b', cd') Else None; k a c b' cd').
proof: Proof. destruct a_opt; simpl; intros; 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