proposition: Lemma to_list_of_list_eq : forall (v : list _), to_list (of_list v) = v.
proof: Proof. induction v; simpl. reflexivity. replace (a :: v) with (a :: to_list (of_list v)). reflexivity. rewrite IHv; reflexivity. 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