proposition: Lemma ByteString_push_word_WS : forall a n front0 bs, ByteString_push_word (WS a front0) bs = ByteString_push a (@ByteString_push_word n front0 bs).
proof: Proof. intros; 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