proposition: Lemma vector_in_map {X Y:Type} (f : X -> Y) n (v : Vector.t X n) y : In y (map f v) -> exists x, In x v /\ f x = y.
proof: Proof. induction v; cbn; try easy. intros [-> | H]%vec_cons_inv. 1: exists h; split; eauto. 1: eapply In_cons_hd. destruct (IHv H) as (x & H1 & H2). exists x. split; eauto. now eapply In_cons_tl. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec PeanoNat) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts