proposition: Lemma enumerator__T_finType {X: finType} : enumerator__T finType_enum X.
proof: Proof. intros x. assert (H := (@enum_ok _ (class X)) x). unfold finType_enum. induction enum as [|y L IH]. - easy. - cbn in H. destruct (Dec (x = y)) as [->|H']. + now exists 0. + destruct (IH H) as [n Hn]. now exists (S n). Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia