proposition: Lemma eq_rect_Vector_cons {A} : forall n m a v H H', eq_rect (S n) (Vector.t A) (Vector.cons A a n v) (S m) H = Vector.cons _ a _ (eq_rect n (Vector.t A) v _ H').
proof: Proof. intros. destruct H'; simpl; symmetry; apply Eqdep_dec.eq_rect_eq_dec; intros; eauto using Peano_dec.eq_nat_dec. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.Peano_dec Coq.Logic.Eqdep_dec Coq.ZArith.ZArith Fiat.Narcissus.Common.Specs Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.Vector Fiat.Narcissus.BinLib.Core Bedrock.Word