proposition: Lemma nat_sat' E : (exists sigma, sat interp_nat sigma (embed_problem E)) <-> H10p E.
proof: Proof. split; intros [sigma ]; exists sigma; now apply nat_sat. Qed.
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