proposition: Lemma ByteString_into_word'_eq : forall bs, bs = word_into_ByteString' (ByteString_into_word' bs).
proof: Proof. induction bs; simpl; f_equal. - 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; unfold eq_rec_r, eq_rec; rewrite <- eq_rect_eq_dec; simpl; eauto using eq_nat_dec. - 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. unfold eq_rec_r, eq_rec; rewrite <- eq_rect_eq_dec; simpl; eauto using eq_nat_dec. 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