proposition: Theorem H10p_to_Q_prv E : H10p E <-> Qeq ⊢I embed E.
proof: Proof. split. - intros. apply Weak with FAeq. now apply H10p_to_FA_prv. firstorder. - intros H%soundness. now apply H10p_to_Q_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