fact: Fixpoint tau2' (A : list (list bool * list bool)) : list bool := match A with | [] => @nil bool | (x,y) :: A0 => y ++ tau2' A0 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)