proposition: Lemma tprep_eval D (I : interp D) rho x t : eval rho (tprep x t) = iprep x (eval rho t).
proof: Proof. induction x; cbn. - reflexivity. - rewrite IHx. reflexivity. 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