proposition: Lemma ByteString_into_queue_eq : forall bs, bs = queue_into_ByteString (ByteString_into_queue bs).
proof: Proof. destruct bs; unfold queue_into_ByteString, ByteString_into_queue; simpl. rewrite <- fold_left_rev_right, rev_app_distr, fold_right_app. induction padding0. - shatter_word front0. rewrite <- (app_nil_l byteString0) at 1. remember nil. replace ByteString_id with {| padding := 0; front := WO; paddingOK := paddingOK0; byteString := l |}. simpl; clear Heql; revert l; induction byteString0; simpl. + intros; rewrite app_nil_r; simpl; repeat f_equal. + intros; rewrite !fold_right_app. simpl. unfold char in a; shatter_word a. unfold ByteString_enqueue at 8; simpl. unfold ByteString_enqueue at 7; simpl. unfold ByteString_enqueue at 6; simpl. unfold ByteString_enqueue at 5; simpl. unfold ByteString_enqueue at 4; simpl. unfold ByteString_enqueue at 3; simpl. unfold ByteString_enqueue at 2; simpl. rewrite app_cons_assoc. rewrite IHbyteString0. repeat f_equal. apply le_uniqueness_proof. + rewrite Heql; unfold ByteString_id; repeat f_equal. apply le_uniqueness_proof. - rewrite (shatter_word front0). simpl. rewrite rev_app_distr, fold_right_app. simpl. assert (lt padding0 8) by omega. erewrite <- (IHpadding0 _ H). unfold ByteString_enqueue; simpl. destruct (eq_nat_dec padding0 7). subst; omega. repeat f_equal. apply le_uniqueness_proof. 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