proposition: Lemma tau1'_spec A : tau1' A = tau1 A.
proof: Proof. induction A as [ | []]; cbn; congruence. 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) Undecidability(PCP)