proposition: Lemma AlignedDecodeBindCharM' {A C : Type} (t : word 8 -> DecodeM (C * ByteString) ByteString) (t' : word 8 -> forall {numBytes}, AlignedDecodeM C numBytes) decode_w : (forall v cd, decode_word (monoidUnit := ByteString_QueueMonoidOpt) (sz := 8) v cd = decode_w v cd) -> (forall b, DecodeMEquivAlignedDecodeM (t b) (@t' b)) -> DecodeMEquivAlignedDecodeM (fun v cd => `(a, b0, cd') <- decode_w v cd; t a b0 cd') (fun numBytes => b <- GetCurrentByte; t' b)%AlignedDecodeM.
proof: Proof. intros; eapply Bind_DecodeMEquivAlignedDecodeM; eauto. eapply DecodeMEquivAlignedDecodeM_trans; eauto. apply AlignedDecodeCharM. simpl. intros; eapply AlignedDecodeMEquiv_refl. 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 Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad