proposition: Lemma NoDupVector_invert {A'} : forall n (l : Vector.t A' n), NoDupVector l -> match l with | Vector.nil => True | Vector.cons a _ l' => ~ Vector.In a l' /\ NoDupVector l' end.
proof: Proof. clear; induction 1; eauto. Qed.
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word