proposition: Lemma WriteB_total' : exists C, forall (c : option (Fin.t n)), projT1 (WriteB c) ↓ fun t k => k >= C.
proof: Proof. eapply fintype_forall_exists; cbn. - intros. eapply TerminatesIn_monotone. { eassumption. } intros ? ? ?. lia. - eapply WriteB_TerminatesIn. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators Undecidability.TM.Compound.WriteString