proposition: Lemma many_vars_S n : many_vars (S n) = n :: many_vars n.
proof: Proof. cbn. f_equal. unfold many_vars. lia. eapply tabulate_ext. intros i. destruct Fin.to_nat as [i_ Hi]. reflexivity. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List