proposition: Lemma standard_embed E rho : standard -> rho ⊨ (embed E) -> H10p E.
proof: Proof. Proof using FA_model. intros HS H. apply standard_embed_problem; trivial. eapply subst_exist_sat2, H. 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