fact: Definition encode_enum (idx : Fin.t _) : CacheFormat -> B * CacheFormat := encode_word (nth tb idx).
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word