proposition: Lemma length_ByteString_push_char : forall (bs' : ByteString) (c : char), length_ByteString (ByteString_push_char c bs') = 8 + (length_ByteString bs').
proof: Proof. intros. 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 ByteString_push_char; simpl. rewrite !length_ByteString_push; repeat f_equal. 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