proposition: Lemma ByteString_into_BitString_eq : forall bs, bs = BitString_into_ByteString (ByteString_into_BitString bs).
proof: Proof. destruct bs; unfold BitString_into_ByteString, ByteString_into_BitString; simpl. induction padding0. - simpl; induction byteString0. + unfold ByteString_id; simpl; repeat f_equal. apply (shatter_word front0). apply le_uniqueness_proof. + simpl; rewrite <- IHbyteString0; simpl. unfold ByteString_push at 8; simpl. unfold ByteString_push at 7; simpl. unfold ByteString_push at 6; simpl. unfold ByteString_push at 5; simpl. unfold ByteString_push at 4; simpl. unfold ByteString_push at 3; simpl. unfold ByteString_push at 2; simpl. unfold ByteString_push at 1; simpl. f_equal. * apply (shatter_word front0). * apply le_uniqueness_proof. * f_equal; unfold eq_rec_r; simpl. rename a into c. pose proof (shatter_word c); simpl in *; pose proof (shatter_word (wtl c)); simpl in *; pose proof (shatter_word (wtl (wtl c))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl c)))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl c))))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl c)))))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl c))))))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl (wtl c)))))))); pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl (wtl (wtl c))))))))); simpl in *. rewrite H, H0, H1, H2, H3, H4, H5, H6, H7; simpl. repeat f_equal. symmetry; apply (shatter_word front0). - pose proof (shatter_word front0) as H'; simpl in H'; rewrite H'; eauto. assert (padding0 < 8)%nat by omega. simpl; erewrite <- (IHpadding0 _ H). unfold ByteString_push; simpl. destruct (eq_nat_dec padding0 7); simpl. exfalso; rewrite e in paddingOK0; eapply Lt.lt_irrefl; eauto. 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