proposition: Lemma tprep_bounded x t n : bounded_t n t -> bounded_t n (tprep x t).
proof: Proof. intros H; induction x; solve_bounds. 1: apply H. apply IHx. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation