proposition: Lemma enumerator__T_bool : enumerator__T bool_enum bool.
proof: Proof. intros []. - now exists 0. - now exists 1. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia