proposition: Lemma problem_to_prv {p : peirce} : forall E sigma, H10p_sem E sigma -> FAeq ⊢ (embed_problem E)[sigma >> num].
proof: Proof. intros [a b] sigma HE. cbn -[FAeq]. eapply transitivity; firstorder. apply prv_poly; firstorder. apply symmetry; firstorder. unfold H10p_sem in *. cbn in HE. rewrite HE. apply prv_poly; firstorder. 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