fact: Fixpoint tabulate_vars n : Vector.t term n := match n with 0 => Vector.nil _ | S n => Vector.cons _ ($0) _ (map (subst_term (S >> var)) (tabulate_vars n)) end.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia