proposition: Lemma AlignedDecode_ifopt {A A' : Type} (decode_A : A' -> DecodeM (A * ByteString) ByteString) (cond : option A') (aligned_decoder : A' -> forall numBytes : nat, AlignedDecodeM A numBytes) : (forall a', DecodeMEquivAlignedDecodeM (decode_A a') (aligned_decoder a')) -> DecodeMEquivAlignedDecodeM (fun bs cd => Ifopt cond as a' Then decode_A a' bs cd Else None) (fun sz => Ifopt cond as a' Then aligned_decoder a' _ 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