proposition: Lemma ByteString_enqueue_ByteString_ByteStringToBoundedByteString : forall bs bs', ByteString_enqueue_ByteString (ByteStringToBoundedByteString bs) (ByteStringToBoundedByteString bs') = ByteStringToBoundedByteString (Core.ByteString_enqueue_ByteString bs bs').
proof: Proof. intros; revert bs; destruct bs'; revert padding0 front0 paddingOK0. unfold ByteStringToBoundedByteString at 2; simpl; intros. unfold ByteString_enqueue_ByteString; simpl. unfold Core.ByteString_enqueue_ByteString; simpl. rewrite ByteStringToBoundedByteString_enqueue_word. f_equal; clear. symmetry; revert bs; induction byteString0. - reflexivity. - intros. pose proof (IHbyteString0 (Core.ByteString_enqueue_char bs a)). replace (fold_left Core.ByteString_enqueue_char (a :: byteString0) bs) with (fold_left Core.ByteString_enqueue_char byteString0 (Core.ByteString_enqueue_char bs a)). rewrite IHbyteString0; simpl. f_equal. apply ByteStringToBoundedByteString_enqueue_word. apply fold_left_cons. 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