proposition: Lemma embed_is_closed E : bounded 0 (embed E).
proof: Proof. unfold embed. rewrite exists_close_form. unfold problem_bound. destruct E as [a b]; cbn. apply (proj2_sig (find_bounded _)). 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