proposition: Lemma problem_to_model E sigma : H10p_sem E sigma -> (sigma >> iμ) ⊨ embed_problem E.
proof: Proof. Proof using FA_model. intros HE%(problem_to_prv (p:=intu))%soundness. specialize (HE D I). setoid_rewrite sat_comp in HE. eapply sat_ext. 2: apply HE. intros x. unfold ">>". now rewrite eval_num. intros. instantiate (1 := (fun _ => iO)). now apply FA_model. 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