proposition: Lemma tabulate_vars_nth n (x : Fin.t n) : Vector.nth (tabulate_vars n) x = $(proj1_sig (Fin.to_nat x)).
proof: Proof. induction n in x|-*. 1: exfalso; revert x; apply Fin.case0. induction x. try easy. cbn. destruct (Fin.to_nat x) as [i P]. cbn in *. erewrite nth_map. 2:easy. rewrite IHx. easy. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia