proposition: Lemma finSucc_opt_Some (n : nat) (i : Fin.t n) : S (fin_to_nat i) < n -> exists i', finSucc_opt i = Some i'.
proof: Proof. induction i; intros; cbn in *. - destruct n. lia. eauto. - destruct n; cbn. lia. rewrite !fin_to_nat_S in *. spec_assert IHi as (i'&IH) by lia. rewrite IH. eauto. Qed.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)