proposition: Lemma bounded_eval_t n t sigma tau : (forall k, n > k -> sigma k = tau k) -> bounded_t n t -> eval sigma t = eval tau t.
proof: Proof. intros H. induction 1; cbn; auto. f_equal. now apply Vector.map_ext_in. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Semantics.Tarski.FullCore Undecidability(Shared.ListAutomation) Vector Lia