fact: Definition finType_enum {X: finType} (n : nat) : option X := nth_error (@enum _ (class X)) n.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia