proposition: Lemma VectorByteToWord_cons : forall n v h H, VectorByteToWord (Vector.cons char h n v) = eq_rect _ _ (Core.append_word (VectorByteToWord v) h) _ H.
proof: Proof. induction v; simpl; intros. rewrite <- !Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. repeat f_equal; apply Eqdep_dec.eq_proofs_unicity; intros; omega. 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 Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality