proposition: Lemma queue_into_ByteString_inj : forall l l', queue_into_ByteString l = queue_into_ByteString l' -> l = l'.
proof: Proof. intros; destruct (queue_into_ByteString_eq_split_BitString l); destruct (queue_into_ByteString_eq_split_BitString l'). eapply split_BitString_inj. rewrite H1, H0 in H; clear H1 H0; injection H. intros; destruct (split_BitString l); destruct (split_BitString l'); simpl in *; subst. f_equal. destruct s; destruct s0; simpl in *. rewrite H1; 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