proposition: Lemma AlignedByteString_dequeue_opt : forall (t : bool) (b b' b'' : ByteString), ByteString_dequeue b = Some (t, b') -> ByteString_dequeue (mappend b b'') = Some (t, mappend b' b'').
proof: Proof. simpl; intros; rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq b), <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq b') in *; rewrite <- (ByteStringToBoundedByteString_BoundedByteStringToByteString_eq b''). rewrite ByteString_dequeue_ByteStringToBoundedByteString_eq in H; destruct (Core.ByteString_dequeue (BoundedByteStringToByteString b)) eqn : ?; simpl in *; try discriminate; destruct p; simpl in *. injection H; intros; subst. apply ByteString_dequeue_mappend_opt with (b'' := BoundedByteStringToByteString b'') in Heqo; simpl in *. rewrite ByteString_enqueue_ByteString_ByteStringToBoundedByteString. rewrite ByteString_dequeue_ByteStringToBoundedByteString_eq. rewrite Heqo; simpl. rewrite ByteString_enqueue_ByteString_ByteStringToBoundedByteString. f_equal; f_equal; f_equal; f_equal. rewrite ByteStringToBoundedByteString_BoundedByteStringToByteString_eq in H. injection H; intros; subst. rewrite BoundedByteStringToByteString_ByteStringToBoundedByteString_eq; reflexivity. 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.Formats.ByteBuffer