proposition: Lemma of_list_to_list : forall (n : nat) (b : t n), of_list (to_list b) = eq_rect n t b (length (to_list b)) (to_list_length n b).
proof: Proof. induction b; simpl. - apply Eqdep_dec.eq_rect_eq_dec; intros; eauto using Peano_dec.eq_nat_dec. - unfold of_list, to_list, Vector.to_list in *. simpl; rewrite IHb; clear. unfold t; erewrite eq_rect_Vector_cons; f_equal. 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