proposition: Lemma Vector_ToList_cons {A} n : forall a (v : Vector.t A n), Vector.to_list (Vector.cons _ a _ v) = a :: Vector.to_list v.
proof: Proof. intros; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction