proposition: Lemma ByteString_enqueue_ByteString_enqueue : forall (l' l : BitString) (b : bool), ByteString_enqueue_ByteString (queue_into_ByteString l) (ByteString_enqueue b (queue_into_ByteString l')) = ByteString_enqueue b (ByteString_enqueue_ByteString (queue_into_ByteString l) (queue_into_ByteString l')).
proof: Proof. intro; destruct (queue_into_ByteString l'). unfold ByteString_enqueue at 1; simpl. destruct (eq_nat_dec padding0 7); simpl. - unfold ByteString_enqueue_ByteString; simpl; subst; clear paddingOK0. intros; rewrite fold_left_app; shatter_word front0; unfold ByteString_enqueue_char; simpl. reflexivity. - 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