fact: Definition EnumType_inj_BoundedIndex {len} {A} {ta} (e : @EnumType len A ta) : BoundedIndex ta := {| indexb := {| ibound := e; boundi := eq_refl |} |}.
imports: Coq.Vectors.Vector Coq.Vectors.Vector Fiat.Common.BoundedLookup