proposition: Lemma enum_term : list_enumerator__T L_term term.
proof: Proof. Proof with eapply cum_ge'; eauto; lia. intros t. induction t. - exists (S n); cbn. apply in_or_app. right. now left. - apply vec_forall_cml in IH as [m H]. 2: exact L_term_cml. exists (S (m + n + ar)); cbn. in_app 3. eapply in_concat. eexists. split. 1: in_collect (n, ar). 1,2: apply L_nat_correct; lia. in_collect v. rewrite <- vecs_from_correct in H |-*. eapply Forall_ext. 2: apply H. cbn. intros... - apply vec_forall_cml in IH as [m H]. 2: exact L_term_cml. destruct (el_T f) as [m' H']. exists (S (m + m')); cbn. in_app 4. eapply in_concat. eexists. split. 1: in_collect f... in_collect v. rewrite <- vecs_from_correct in H |-*. eapply Forall_ext. 2: apply H. cbn. intros... Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List