proposition: Lemma vecs_from_correct X (A : list X) (n : nat) (v : vec X n) : VectorForall.Forall (fun x => x el A) v <-> v el vecs_from A n.
proof: Proof. induction n; cbn. - split. + intros. left. pattern v. now apply Vector.case0. + now intros [<-|[]]. - split. + intros. revert H. apply (Vector.caseS' v). intros. in_collect (h, t); destruct (IHn t). apply H. apply H0. apply H. + intros Hv. apply in_map_iff in Hv as ([h v'] & <- & (? & ? & [= <- <-] & ? & ?) % list_prod_in). split. easy. destruct (IHn v'). now apply H2. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List