proposition: Fact numeral_subst_invariance n rho : subst_term rho (num n) = num n.
proof: Proof. induction n. - reflexivity. - cbn. now rewrite IHn. 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