proposition: Lemma aligned_decode_unused_char_eq' {numBytes} : forall (v : Vector.t _ (S numBytes)) env, WordOpt.decode_unused_word (sz := 8) (monoidUnit := ByteString_QueueMonoidOpt) (build_aligned_ByteString v) env = Some ((), build_aligned_ByteString (Vector.tl v), addD env 8).
proof: Proof. unfold decode_unused_word; simpl; intros. etransitivity. unfold Compose_Decode, DecodeBindOpt. unfold BindOpt. eapply AlignedDecodeChar. pattern numBytes, v. eapply Vector.caseS; simpl; intros. reflexivity. 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