proposition: Lemma ByteString_enqueue_ByteString_into_BitString : forall (l' l : BitString), ByteString_enqueue_ByteString (queue_into_ByteString l) (queue_into_ByteString l') = queue_into_ByteString (l ++ l').
proof: Proof. intro; generalize (le_refl (length l')); remember (length l'). setoid_rewrite Heqn at 1; clear Heqn; revert l'; induction n. - intros; destruct l'; simpl; intros. + rewrite ByteString_enqueue_ByteString_id_right, app_nil_r; reflexivity. + inversion H. - intros; rewrite queue_into_ByteString_app. rewrite <- (rev_involutive l') in *. clear IHn H. induction (rev l'); simpl. + rewrite ByteString_enqueue_ByteString_id_right; reflexivity. + rewrite <- ByteString_enqueue_into_BitString. rewrite fold_left_app; simpl. rewrite <- IHl0. apply ByteString_enqueue_ByteString_enqueue. 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