proposition: Lemma Step_total' : exists C, forall q, projT1 (Step q) ↓ fun t k => C <= k.
proof: Proof. eapply fintype_forall_exists. - intros. eapply TerminatesIn_monotone. { eassumption. } intros ? ?. lia. - intros q. eapply Step_total. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString