proposition: Lemma ByteString_enqueue_ByteString_enqueue_ByteString : forall (b : bool) (b' b'' : ByteString), ByteString_enqueue b (ByteString_enqueue_ByteString b' b'') = ByteString_enqueue_ByteString b' (ByteString_enqueue b b'').
proof: Proof. intros; rewrite (ByteString_into_queue_eq b'), (ByteString_into_queue_eq b''), !ByteString_enqueue_ByteString_into_BitString, !ByteString_enqueue_into_BitString. replace [b] with (ByteString_into_queue (ByteString_enqueue b ByteString_id)) by reflexivity. rewrite !ByteString_enqueue_ByteString_into_BitString, app_assoc; 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