proposition: Lemma BindAlignedDecodeM_assoc {A B C : Type} {n}: forall (a : AlignedDecodeM A n) (f : A -> AlignedDecodeM B n) (g : B -> AlignedDecodeM C n), AlignedDecodeMEquiv (BindAlignedDecodeM (BindAlignedDecodeM a f) g) (BindAlignedDecodeM a (fun a => BindAlignedDecodeM (f a) g)).
proof: Proof. unfold BindAlignedDecodeM, AlignedDecodeMEquiv; simpl; intros. destruct (a v idx c); simpl; eauto. 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