fact: Definition sdec_PCPb := (fun (P : PCP.stack bool) n => match stack_enum n with Some [] | None => false | Some A => andb (subsetb A P) (blist_eqb (tau1' A) (tau2' A)) end).
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) Undecidability(PCP)