proposition: Lemma enumerator__T_Fin {k: nat} : enumerator__T Fin_enum (Fin.t k).
proof: Proof. intros t. exists (proj1_sig (Fin.to_nat t)). unfold Fin_enum. induction t as [n|n t IH]. { reflexivity. } cbn. destruct (Fin.to_nat t) as [t' H']. cbn in *. now rewrite nth_error_map, IH. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia