proposition: Lemma prv_poly {p : peirce} sigma q Gamma : incl FAeq Gamma -> Gamma ⊢ ( (embed_poly q)`[sigma >> num] == num (dp_eval_pfree sigma q) ).
proof: Proof. intros H. induction q; cbn. - change ((num n)`[sigma >> num]) with (subst_term (sigma >> num) (num n)). rewrite numeral_subst_invariance. now apply reflexivity. - now apply reflexivity. - destruct d; cbn. + eapply transitivity. assumption. apply (eq_add H IHq1 IHq2). now apply num_add_homomorphism. + eapply transitivity. assumption. apply (eq_mult H IHq1 IHq2). now apply num_mult_homomorphism. 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