proposition: Lemma fintype_forall_exists (F : finType) (P : F -> nat -> Prop) : (forall x n, P x n -> forall m, m >= n -> P x m) -> (forall x : F, exists n, P x n) -> exists N, forall x, P x N.
proof: Proof. intros P_mono FE. destruct (fintype_choice FE) as [f Hf]. exists (list_sum (map f (elem F))). intros x. apply (P_mono x _ (Hf x)). destruct (in_split _ _ (elem_spec x)) as [? [? ->]]. rewrite map_app, list_sum_app. cbn. lia. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString