proposition: Lemma enum_form {ff : falsity_flag} : list_enumerator__T L_form form.
proof: Proof. Proof with (try eapply cum_ge'; eauto; lia). intros phi. induction phi. - exists 1. cbn; eauto. - rename t into v. destruct (el_T P) as [m Hm], (@vec_forall_cml term L_term _ v) as [m' Hm']; eauto using enum_term. exists (S (m + m')); cbn. in_app 2. eapply in_concat. eexists. split. 1: eapply in_map_iff; exists P. 1: repeat split. 1: idtac... eapply in_map. rewrite <- vecs_from_correct in *. intuition... - destruct (el_T b0) as [m Hm], IHphi1 as [m1], IHphi2 as [m2]. exists (1 + m + m1 + m2). cbn. in_app 3. apply in_concat. eexists. split. apply in_map... in_collect (pair phi1 phi2)... - destruct (el_T q) as [m Hm], IHphi as [m' Hm']. exists (1 + m + m'). cbn -[L_T]. in_app 4. apply in_concat. eexists. split. apply in_map... in_collect phi... 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