proposition: Lemma vec_forall_cml X (L : nat -> list X) n (v : vec X n) : cumulative L -> (VectorForall.Forall (fun x => exists m, x el L m) v) -> exists m, v el vecs_from (L m) n.
proof: Proof. intros HL Hv. induction v; cbn. - exists 0. now left. - destruct IHv as [m H], Hv as [[m' H'] Hv]. easy. exists (m + m'). in_collect (h, v). apply (cum_ge' (n:=m')); intuition lia. apply vecs_from_correct. rewrite <- vecs_from_correct in H. eapply Forall_ext. 2: apply H. cbn. intros x Hx. apply (cum_ge' (n:=m)). all: eauto. lia. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List