fact: Definition embed_problem (E : H10p_PROBLEM) : form := let (a, b) := E in embed_poly a == embed_poly b.
imports: Undecidability.Synthetic.Definitions Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullFacts Semantics.Tarski.FullSoundness) Undecidability.FOL.PA Undecidability.FOL.Arithmetics(TarskiFacts DeductionFacts NatModel) Undecidability.H10(H10p) List Lia