proposition: Lemma massage_queue_into_ByteString : forall n w1 paddingOK' paddingOK'' paddingOK''' l' l, {| padding := n; front := w1; paddingOK := paddingOK'; byteString := l ++ l' |} = ByteString_enqueue_ByteString {| padding := 0; front := WO; paddingOK := paddingOK'''; byteString := l|} {| padding := n; front := w1; paddingOK := paddingOK''; byteString := l' |}.
proof: Proof. induction l'. - simpl. intros; rewrite app_nil_r. unfold ByteString_enqueue_ByteString; simpl. destruct n as [ | [ | [ | [ | [ | [ | [ | [ | ] ] ] ] ] ] ] ]; try solve [inversion paddingOK']; try shatter_word w1; simpl; unfold queue_into_ByteString; simpl; repeat f_equal. + apply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue, ByteString_enqueue; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue, ByteString_enqueue; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 4; simpl. unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl. unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id, ByteString_dequeue; simpl. unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + unfold queue_into_ByteString, ByteString_id; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. repeat f_equal; eapply le_uniqueness_proof. + omega. - intros. rewrite app_cons_assoc. simpl. pose proof (IHl' (l ++ [a])) as e; simpl in e; rewrite e; clear e IHl'. unfold ByteString_enqueue_ByteString; simpl. f_equal. unfold ByteString_enqueue_char at 3; simpl. unfold ByteString_enqueue at 7; simpl; unfold ByteString_enqueue at 6; simpl; unfold ByteString_enqueue at 5; simpl; unfold ByteString_enqueue at 4; simpl; unfold ByteString_enqueue at 3; simpl; unfold ByteString_enqueue at 2; simpl; unfold ByteString_enqueue at 1; simpl. unfold char in *. shatter_word a. 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