proposition: Lemma stack_enum : enumerable__T (stack bool).
proof: Proof. unfold stack. eapply enumerator_enumerable, enumerator__T_to_list, enumerator__T_list, enumerator__T_of_list, enumerator__T_prod. all: eapply enumerator__T_to_list, enumerator__T_list. all: eapply enumerator__T_of_list, enumerator__T_bool. Qed.
imports: List Undecidability.PCP.PCP Undecidability.PCP.Util.Facts Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts MoreEnumerabilityFacts ListEnumerabilityFacts) Coq.Init.Wf Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite)