proposition: Lemma AlignedDecodeBindUnused2CharM {C : Type} (t : unit -> DecodeM (C * _) ByteString) (t' : unit -> forall {numBytes}, AlignedDecodeM C numBytes) : (DecodeMEquivAlignedDecodeM (t ()) (@t' ())) -> DecodeMEquivAlignedDecodeM (fun v cd => `(a, b0, cd') <- decode_unused_word (monoidUnit := ByteString_QueueMonoidOpt) (sz := 16) v cd; t a b0 cd') (fun numBytes => b <- SkipCurrentByte; b <- SkipCurrentByte; @t' b numBytes)%AlignedDecodeM.
proof: Proof. intro. eapply DecodeMEquivAlignedDecodeM_trans. eapply Bind_DecodeMEquivAlignedDecodeM. eapply AlignedDecodeNUnusedCharM with (m := 2); eauto. intros [ ]; eassumption. reflexivity. intros; simpl. unfold AlignedDecodeMEquiv, BindAlignedDecodeM; simpl; intros. destruct (SkipCurrentByte v idx c) as [ [ [? ?] ] | ]; simpl; eauto. destruct (SkipCurrentByte v n0 c0) as [ [ [? ?] ] | ]; simpl; eauto. destruct u0; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word