proposition: Lemma rho_from_vec_map {A B} {n} (f : B -> A) (t : Vector.t B n) (d2 : A) (d:B): f d = d2 -> forall k, rho_from_vec (map f t) d2 k = f (rho_from_vec t d k).
proof: Proof. intros H k. unfold rho_from_vec. destruct (Compare_dec.lt_dec k n) as [Hl|Hr]. - erewrite nth_map. 2:reflexivity. easy. - easy. Qed.
imports: Undecidability.FOL.Syntax.Facts Undecidability.FOL.Syntax.Theories Undecidability.FOL.Semantics.Tarski.FragmentCore Undecidability(Shared.ListAutomation) Vector Lia