proposition: Lemma semantic_lifting_correct n t tt : map (subst_term (rho_from_vec t tt)) (tabulate_vars n) = t.
proof: Proof. apply eq_nth_iff. intros i ? <-. erewrite nth_map. 2:reflexivity. rewrite tabulate_vars_nth. cbn. unfold rho_from_vec. destruct (Fin.to_nat i) as [i2 P2] eqn:Heq; cbn. destruct Compare_dec.lt_dec; try lia. f_equal. erewrite <- Fin.of_nat_to_nat_inv. rewrite Heq. cbn. apply Fin.of_nat_ext. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia