proposition: Lemma stack_enum_spec : enumerator__T stack_enum (PCP.stack bool).
proof: Proof. exact _. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts ListEnumerabilityFacts) Lia Undecidability.L(LProd LBool LNat LOptions) Undecidability.L.Datatypes.List(List_basics List_eqb List_extra List_nat)