fact: Fixpoint subst_term (σ : nat -> term) (t : term) : term := match t with | var t => σ t | func f v => func f (map (subst_term σ) v) end.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors)