proposition: Theorem H10p_to_FA_sat E : H10p E <-> valid_ctx FAeq (embed E).
proof: Proof. split. - intros [sigma HE]. intros D I rho H. eapply subst_exist_sat. apply problem_to_model. + intros ρ' ax Hax. eapply sat_closed. 2: now apply H. repeat (destruct Hax as [<- | Hax]; cbn; repeat solve_bounds; auto). inversion Hax. + apply HE. + rewrite <-exists_close_form; apply embed_is_closed. - intros H. specialize (H nat interp_nat id (nat_is_FA_model id)). unfold embed in *. apply subst_exist_sat2 in H. 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