proposition: Lemma enum_form : list_enumerator__T L_form form.
proof: Proof. Proof with eapply cum_ge'; eauto; lia. intros phi. induction phi. - exists 0. now left. - rename t into v. destruct (@vec_forall_cml term L_term _ v) as [m H]; eauto. + clear p. induction v. easy. split. apply enum_term. apply IHv. + destruct p; cbn. * exists (S (m + n + ar)); cbn. in_app 2. 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... * destruct (el_T P) as [m']. exists (S (m + m')); cbn. in_app 3. eapply in_concat. eexists. split. 1: in_collect P... in_collect v. rewrite <- vecs_from_correct in H |-*. eapply Forall_ext. 2: apply H. cbn. intros... - destruct (el_T b) as [m], IHphi1 as [m1], IHphi2 as [m2]. exists (1 + m + m1 + m2); cbn. in_app 4. apply in_concat. eexists. split. in_collect b... in_collect (phi1, phi2)... - destruct (el_T q) as [m], IHphi as [m']. exists (S (m + m')); cbn. in_app 5. apply in_concat. eexists. split. in_collect q... in_collect phi... - destruct (el_T q) as [m], IHphi as [m']. exists (S (m + m' + n)); cbn. in_app 6. apply in_concat. eexists. split. in_collect (q, n). eapply cum_ge'; eauto; lia. apply L_nat_correct; lia. in_collect phi... - destruct (el_T q) as [m], IHphi as [m']. exists (S (m + m' + n)); cbn. in_app 7. apply in_concat. eexists. split. in_collect (q, n). eapply cum_ge'; eauto; lia. apply L_nat_correct; lia. in_collect phi... Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List