proposition: Lemma ByteString_dequeue_head_opt : forall t, ByteString_dequeue (ByteString_enqueue t ByteString_id) = Some (t, ByteString_id).
proof: Proof. intros; unfold ByteString_enqueue, ByteString_id, ByteString_dequeue; simpl; 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