proposition: Lemma vec_forall_cml X (L : nat -> list X) n (v : vec X n) : cumulative L -> (forall x, InT x v -> exists m, x el L m) -> exists m, v el vecs_from (L m) n.
proof: Proof. intros HL Hv. induction v; cbn. - exists 0. tauto. - destruct IHv as [m H], (Hv h) as [m' H']. 1,3:now left. + intros x Hx. apply Hv. now right. + exists (m + m'). in_collect (pair h v). 1: apply (cum_ge' (n:=m')); intuition lia. apply vecs_from_correct. rewrite <- vecs_from_correct in H. intros x Hx. apply (cum_ge' (n:=m)). all: eauto. lia. 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