fact: Fixpoint shift `{funcs_signature} `{preds_signature} n (t : term) := match n with | O => t | S n => subst_term ↑ (shift n t) end.
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.FOL.Sets.Signatures List