proposition: Corollary H10_to_entailment_PA : H10p ⪯ entailment_PA.
proof: Proof. exists embed; intros E. apply H10p_to_PA_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