proposition: Theorem H10p_to_FA_prv' {p : peirce} E : H10p E -> FAeq ⊢ embed E.
proof: Proof. intros [sigma HE]. eapply subst_exist_prv. apply problem_to_prv, HE. rewrite <-exists_close_form; apply embed_is_closed. 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