proposition: Lemma problem_to_ext_model : forall E sigma, H10p_sem E sigma -> (sigma >> iμ) ⊨ embed_problem E.
proof: Proof. Proof using ext_model FA_model. intros [a b] sigma Hs. cbn -[sat]. unfold H10p_sem in *. cbn -[FA] in *. apply ext_model. rewrite !eval_poly. congruence. 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