proposition: Lemma vecs_from_correct X (A : list X) (n : nat) (v : vec X n) : (forall x, InT x v -> x el A) <-> v el vecs_from A n.
proof: Proof. induction n; cbn. - split. + intros. left. pattern v. now apply Vector.case0. + intros [<- | []] x H. inv H. - split. + intros. revert H. apply (Vector.caseS' v). clear v. intros ? t0 H. in_collect (pair h t0); destruct (IHn t0). 1: eapply H; now left. apply H0. intros x Hx. apply H. now right. + intros Hv. apply in_map_iff in Hv as ([h v'] & <- & (? & ? & [= <- <-] & ? & ?) % list_prod_in). intros x H. inv H; destruct (IHn v'); eauto. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts