proposition: Fact nat_eval_poly (sigma : env nat) p : @eval _ _ _ interp_nat sigma (embed_poly p) = dp_eval_pfree sigma p.
proof: Proof. induction p; cbn. - now rewrite nat_eval_num. - reflexivity. - destruct d; cbn. + now rewrite IHp1, IHp2. + now rewrite IHp1, IHp2. 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