proposition: Lemma AlignedDecode_ifb {A : Type} (decode_A : DecodeM (A * ByteString) ByteString) (cond : bool) (aligned_decoder : forall numBytes : nat, AlignedDecodeM A numBytes) : DecodeMEquivAlignedDecodeM decode_A aligned_decoder -> DecodeMEquivAlignedDecodeM (fun bs cd => if cond then decode_A bs cd else None) (fun sz => if cond then aligned_decoder sz else ThrowAlignedDecodeM).
proof: Proof. intros; destruct cond; simpl; eauto using AlignedDecode_Throw. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString