proposition: Lemma enum_recalg n: list_enumerator__T (L_recalg n) (recalg n).
proof: Proof. intros t. induction t as [k| | |k p|k i t gj [m1 IHt] IHgj|k t1 t2 [m1 IH1] [m2 IH2]|k t [m IHt]] using recalg_rect. - exists (S k). walklist 1. easy. - exists 1. walklist 2. easy. - exists 1. walklist 3. easy. - exists 1. walklist 4. apply in_map. induction p; cbn. 1: now left. right. now apply in_map. - destruct (exists_max _ _ IHgj) as [m2 Hm2]. exists (S (max3 k m1 m2)). walklist 5. rewrite match_n_spec. eapply in_concat. exists (concat [concat [@ra_comp k i v1 v2 :: nil | v2 ∈ list_vectors _ k (L_recalg i (max3 k m1 m2))] | v1 ∈ L_recalg k (max3 k m1 m2)]). split. 1: { apply in_map_iff. exists k. split; try easy. apply list_le_spec. unfold max3. lia. } eapply in_concat. exists (concat [@ra_comp k i t v2 :: nil| v2 ∈ list_vectors _ k (L_recalg i (max3 k m1 m2))]). split. 1: { apply in_map_iff. exists t. split; try easy. eapply cum_ge'. 1: apply L_recalg_cml. 1: apply IHt. unfold max3; lia. } eapply in_concat. exists [@ra_comp k i t gj]. split. + eapply in_map_iff. exists gj; split; try easy. eapply list_vectors_spec. intros p. destruct (Hm2 p) as [idx [Hidx Hmidx]]. eapply cum_ge'. 1: apply L_recalg_cml. 1: apply Hidx. unfold max3; lia. + now left. - exists (S (max m1 m2)). walklist 6. eapply in_concat. eexists (concat [ra_rec v1 t2::nil | v1 ∈ L_recalg k (max m1 m2)]). split. 1: { apply in_map_iff. exists t2. split; try easy. eapply cum_ge'. 1: apply L_recalg_cml. 1: apply IH2. lia. } eapply in_concat. eexists (ra_rec t1 t2::nil). split. 2: now left. eapply in_map_iff. exists t1. split; try easy. eapply cum_ge'. 1: apply L_recalg_cml. 1: apply IH1. lia. - exists (S m). walklist 7. rewrite match_n_spec. eapply in_concat. eexists [_]. split. 2: now left. eapply in_map_iff. exists t. split. 1:easy. apply IHt. Qed.
imports: Arith Lia List Bool Eqdep_dec EqdepFacts Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list finite pos vec) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Undecidability.MuRec.Util.recalg